Definition: Formco
`Formco(C) ==`
`  corec(X.lbl:Atom × if lbl =a "Var" then Atom`
`                     if lbl =a "Const" then C`
`                     if lbl =a "Set" then var:Atom × X`
`                     if lbl =a "Equal" then left:X × X`
`                     if lbl =a "Member" then element:X × X`
`                     if lbl =a "And" then left:X × X`
`                     if lbl =a "Or" then left:X × X`
`                     if lbl =a "Not" then X`
`                     if lbl =a "All" then var:Atom × X`
`                     if lbl =a "Exists" then var:Atom × X`
`                     else Void`
`                     fi )`

Lemma: Formco_wf
`∀[C:Type]. (Formco(C) ∈ Type)`

Lemma: Formco-ext
`∀[C:Type]`
`  Formco(C) ≡ lbl:Atom × if lbl =a "Var" then Atom`
`                         if lbl =a "Const" then C`
`                         if lbl =a "Set" then var:Atom × Formco(C)`
`                         if lbl =a "Equal" then left:Formco(C) × Formco(C)`
`                         if lbl =a "Member" then element:Formco(C) × Formco(C)`
`                         if lbl =a "And" then left:Formco(C) × Formco(C)`
`                         if lbl =a "Or" then left:Formco(C) × Formco(C)`
`                         if lbl =a "Not" then Formco(C)`
`                         if lbl =a "All" then var:Atom × Formco(C)`
`                         if lbl =a "Exists" then var:Atom × Formco(C)`
`                         else Void`
`                         fi `

Definition: Formco_size
`Formco_size(p) ==`
`  fix((λsize,p. let lbl,x = p `
`                in if lbl =a "Var" then 0`
`                   if lbl =a "Const" then 0`
`                   if lbl =a "Set" then 1 + (size (snd(x)))`
`                   if lbl =a "Equal" then 1 + (size (fst(x))) + (size (snd(x)))`
`                   if lbl =a "Member" then 1 + (size (fst(x))) + (size (snd(x)))`
`                   if lbl =a "And" then 1 + (size (fst(x))) + (size (snd(x)))`
`                   if lbl =a "Or" then 1 + (size (fst(x))) + (size (snd(x)))`
`                   if lbl =a "Not" then 1 + (size x)`
`                   if lbl =a "All" then 1 + (size (snd(x)))`
`                   if lbl =a "Exists" then 1 + (size (snd(x)))`
`                   else 0`
`                   fi )) `
`  p`

Lemma: Formco_size_wf
`∀[C:Type]. ∀[p:Formco(C)].  (Formco_size(p) ∈ partial(ℕ))`

Definition: Form
`Form(C) ==  {p:Formco(C)| (Formco_size(p))↓} `

Lemma: Form_wf
`∀[C:Type]. (Form(C) ∈ Type)`

Definition: Form_size
`Form_size(p) ==`
`  fix((λsize,p. let lbl,x = p `
`                in if lbl =a "Var" then 0`
`                   if lbl =a "Const" then 0`
`                   if lbl =a "Set" then 1 + (size (snd(x)))`
`                   if lbl =a "Equal" then 1 + (size (fst(x))) + (size (snd(x)))`
`                   if lbl =a "Member" then 1 + (size (fst(x))) + (size (snd(x)))`
`                   if lbl =a "And" then 1 + (size (fst(x))) + (size (snd(x)))`
`                   if lbl =a "Or" then 1 + (size (fst(x))) + (size (snd(x)))`
`                   if lbl =a "Not" then 1 + (size x)`
`                   if lbl =a "All" then 1 + (size (snd(x)))`
`                   if lbl =a "Exists" then 1 + (size (snd(x)))`
`                   else 0`
`                   fi )) `
`  p`

Lemma: Form_size_wf
`∀[C:Type]. ∀[p:Form(C)].  (Form_size(p) ∈ ℕ)`

Lemma: Form-ext
`∀[C:Type]`
`  Form(C) ≡ lbl:Atom × if lbl =a "Var" then Atom`
`                       if lbl =a "Const" then C`
`                       if lbl =a "Set" then var:Atom × Form(C)`
`                       if lbl =a "Equal" then left:Form(C) × Form(C)`
`                       if lbl =a "Member" then element:Form(C) × Form(C)`
`                       if lbl =a "And" then left:Form(C) × Form(C)`
`                       if lbl =a "Or" then left:Form(C) × Form(C)`
`                       if lbl =a "Not" then Form(C)`
`                       if lbl =a "All" then var:Atom × Form(C)`
`                       if lbl =a "Exists" then var:Atom × Form(C)`
`                       else Void`
`                       fi `

Definition: FormVar
`Vname ==  <"Var", name>`

Lemma: FormVar_wf
`∀[C:Type]. ∀[name:Atom].  (Vname ∈ Form(C))`

Definition: FormConst
`Const(value) ==  <"Const", value>`

Lemma: FormConst_wf
`∀[C:Type]. ∀[value:C].  (Const(value) ∈ Form(C))`

Definition: FormSet
`{var | phi} ==  <"Set", var, phi>`

Lemma: FormSet_wf
`∀[C:Type]. ∀[var:Atom]. ∀[phi:Form(C)].  ({var | phi} ∈ Form(C))`

Definition: FormEqual
`left = right ==  <"Equal", left, right>`

Lemma: FormEqual_wf
`∀[C:Type]. ∀[left,right:Form(C)].  (left = right ∈ Form(C))`

Definition: FormMember
`element ∈ set ==  <"Member", element, set>`

Lemma: FormMember_wf
`∀[C:Type]. ∀[element,set:Form(C)].  (element ∈ set ∈ Form(C))`

Definition: FormAnd
`left ∧ right) ==  <"And", left, right>`

Lemma: FormAnd_wf
`∀[C:Type]. ∀[left,right:Form(C)].  (left ∧ right) ∈ Form(C))`

Definition: FormOr
`left ∨ right ==  <"Or", left, right>`

Lemma: FormOr_wf
`∀[C:Type]. ∀[left,right:Form(C)].  (left ∨ right ∈ Form(C))`

Definition: FormNot
`¬(body) ==  <"Not", body>`

Lemma: FormNot_wf
`∀[C:Type]. ∀[body:Form(C)].  (¬(body) ∈ Form(C))`

Definition: FormAll
`∀var. body ==  <"All", var, body>`

Lemma: FormAll_wf
`∀[C:Type]. ∀[var:Atom]. ∀[body:Form(C)].  (∀var. body ∈ Form(C))`

Definition: FormExists
`∃var. body ==  <"Exists", var, body>`

Lemma: FormExists_wf
`∀[C:Type]. ∀[var:Atom]. ∀[body:Form(C)].  (∃var. body ∈ Form(C))`

Definition: FormVar?
`FormVar?(v) ==  fst(v) =a "Var"`

Lemma: FormVar?_wf
`∀[C:Type]. ∀[v:Form(C)].  (FormVar?(v) ∈ 𝔹)`

Definition: FormVar-name
`FormVar-name(v) ==  snd(v)`

Lemma: FormVar-name_wf
`∀[C:Type]. ∀[v:Form(C)].  FormVar-name(v) ∈ Atom supposing ↑FormVar?(v)`

Definition: FormConst?
`FormConst?(v) ==  fst(v) =a "Const"`

Lemma: FormConst?_wf
`∀[C:Type]. ∀[v:Form(C)].  (FormConst?(v) ∈ 𝔹)`

Definition: FormConst-value
`FormConst-value(v) ==  snd(v)`

Lemma: FormConst-value_wf
`∀[C:Type]. ∀[v:Form(C)].  FormConst-value(v) ∈ C supposing ↑FormConst?(v)`

Definition: FormSet?
`FormSet?(v) ==  fst(v) =a "Set"`

Lemma: FormSet?_wf
`∀[C:Type]. ∀[v:Form(C)].  (FormSet?(v) ∈ 𝔹)`

Definition: FormSet-var
`FormSet-var(v) ==  fst(snd(v))`

Lemma: FormSet-var_wf
`∀[C:Type]. ∀[v:Form(C)].  FormSet-var(v) ∈ Atom supposing ↑FormSet?(v)`

Definition: FormSet-phi
`FormSet-phi(v) ==  snd(snd(v))`

Lemma: FormSet-phi_wf
`∀[C:Type]. ∀[v:Form(C)].  FormSet-phi(v) ∈ Form(C) supposing ↑FormSet?(v)`

Definition: FormEqual?
`FormEqual?(v) ==  fst(v) =a "Equal"`

Lemma: FormEqual?_wf
`∀[C:Type]. ∀[v:Form(C)].  (FormEqual?(v) ∈ 𝔹)`

Definition: FormEqual-left
`FormEqual-left(v) ==  fst(snd(v))`

Lemma: FormEqual-left_wf
`∀[C:Type]. ∀[v:Form(C)].  FormEqual-left(v) ∈ Form(C) supposing ↑FormEqual?(v)`

Definition: FormEqual-right
`FormEqual-right(v) ==  snd(snd(v))`

Lemma: FormEqual-right_wf
`∀[C:Type]. ∀[v:Form(C)].  FormEqual-right(v) ∈ Form(C) supposing ↑FormEqual?(v)`

Definition: FormMember?
`FormMember?(v) ==  fst(v) =a "Member"`

Lemma: FormMember?_wf
`∀[C:Type]. ∀[v:Form(C)].  (FormMember?(v) ∈ 𝔹)`

Definition: FormMember-element
`FormMember-element(v) ==  fst(snd(v))`

Lemma: FormMember-element_wf
`∀[C:Type]. ∀[v:Form(C)].  FormMember-element(v) ∈ Form(C) supposing ↑FormMember?(v)`

Definition: FormMember-set
`FormMember-set(v) ==  snd(snd(v))`

Lemma: FormMember-set_wf
`∀[C:Type]. ∀[v:Form(C)].  FormMember-set(v) ∈ Form(C) supposing ↑FormMember?(v)`

Definition: FormAnd?
`FormAnd?(v) ==  fst(v) =a "And"`

Lemma: FormAnd?_wf
`∀[C:Type]. ∀[v:Form(C)].  (FormAnd?(v) ∈ 𝔹)`

Definition: FormAnd-left
`FormAnd-left(v) ==  fst(snd(v))`

Lemma: FormAnd-left_wf
`∀[C:Type]. ∀[v:Form(C)].  FormAnd-left(v) ∈ Form(C) supposing ↑FormAnd?(v)`

Definition: FormAnd-right
`FormAnd-right(v) ==  snd(snd(v))`

Lemma: FormAnd-right_wf
`∀[C:Type]. ∀[v:Form(C)].  FormAnd-right(v) ∈ Form(C) supposing ↑FormAnd?(v)`

Definition: FormOr?
`FormOr?(v) ==  fst(v) =a "Or"`

Lemma: FormOr?_wf
`∀[C:Type]. ∀[v:Form(C)].  (FormOr?(v) ∈ 𝔹)`

Definition: FormOr-left
`FormOr-left(v) ==  fst(snd(v))`

Lemma: FormOr-left_wf
`∀[C:Type]. ∀[v:Form(C)].  FormOr-left(v) ∈ Form(C) supposing ↑FormOr?(v)`

Definition: FormOr-right
`FormOr-right(v) ==  snd(snd(v))`

Lemma: FormOr-right_wf
`∀[C:Type]. ∀[v:Form(C)].  FormOr-right(v) ∈ Form(C) supposing ↑FormOr?(v)`

Definition: FormNot?
`FormNot?(v) ==  fst(v) =a "Not"`

Lemma: FormNot?_wf
`∀[C:Type]. ∀[v:Form(C)].  (FormNot?(v) ∈ 𝔹)`

Definition: FormNot-body
`FormNot-body(v) ==  snd(v)`

Lemma: FormNot-body_wf
`∀[C:Type]. ∀[v:Form(C)].  FormNot-body(v) ∈ Form(C) supposing ↑FormNot?(v)`

Definition: FormAll?
`FormAll?(v) ==  fst(v) =a "All"`

Lemma: FormAll?_wf
`∀[C:Type]. ∀[v:Form(C)].  (FormAll?(v) ∈ 𝔹)`

Definition: FormAll-var
`FormAll-var(v) ==  fst(snd(v))`

Lemma: FormAll-var_wf
`∀[C:Type]. ∀[v:Form(C)].  FormAll-var(v) ∈ Atom supposing ↑FormAll?(v)`

Definition: FormAll-body
`FormAll-body(v) ==  snd(snd(v))`

Lemma: FormAll-body_wf
`∀[C:Type]. ∀[v:Form(C)].  FormAll-body(v) ∈ Form(C) supposing ↑FormAll?(v)`

Definition: FormExists?
`FormExists?(v) ==  fst(v) =a "Exists"`

Lemma: FormExists?_wf
`∀[C:Type]. ∀[v:Form(C)].  (FormExists?(v) ∈ 𝔹)`

Definition: FormExists-var
`FormExists-var(v) ==  fst(snd(v))`

Lemma: FormExists-var_wf
`∀[C:Type]. ∀[v:Form(C)].  FormExists-var(v) ∈ Atom supposing ↑FormExists?(v)`

Definition: FormExists-body
`FormExists-body(v) ==  snd(snd(v))`

Lemma: FormExists-body_wf
`∀[C:Type]. ∀[v:Form(C)].  FormExists-body(v) ∈ Form(C) supposing ↑FormExists?(v)`

Lemma: Form-induction
`∀[C:Type]. ∀[P:Form(C) ⟶ ℙ].`
`  ((∀name:Atom. P[Vname])`
`  `` (∀value:C. P[Const(value)])`
`  `` (∀var:Atom. ∀phi:Form(C).  (P[phi] `` P[{var | phi}]))`
`  `` (∀left,right:Form(C).  (P[left] `` P[right] `` P[left = right]))`
`  `` (∀element,set:Form(C).  (P[element] `` P[set] `` P[element ∈ set]))`
`  `` (∀left,right:Form(C).  (P[left] `` P[right] `` P[left ∧ right)]))`
`  `` (∀left,right:Form(C).  (P[left] `` P[right] `` P[left ∨ right]))`
`  `` (∀body:Form(C). (P[body] `` P[¬(body)]))`
`  `` (∀var:Atom. ∀body:Form(C).  (P[body] `` P[∀var. body]))`
`  `` (∀var:Atom. ∀body:Form(C).  (P[body] `` P[∃var. body]))`
`  `` {∀v:Form(C). P[v]})`

Lemma: Form-definition
`∀[C,A:Type]. ∀[R:A ⟶ Form(C) ⟶ ℙ].`
`  ((∀name:Atom. {x:A| R[x;Vname]} )`
`  `` (∀value:C. {x:A| R[x;Const(value)]} )`
`  `` (∀var:Atom. ∀phi:Form(C).  ({x:A| R[x;phi]}  `` {x:A| R[x;{var | phi}]} ))`
`  `` (∀left,right:Form(C).  ({x:A| R[x;left]}  `` {x:A| R[x;right]}  `` {x:A| R[x;left = right]} ))`
`  `` (∀element,set:Form(C).  ({x:A| R[x;element]}  `` {x:A| R[x;set]}  `` {x:A| R[x;element ∈ set]} ))`
`  `` (∀left,right:Form(C).  ({x:A| R[x;left]}  `` {x:A| R[x;right]}  `` {x:A| R[x;left ∧ right)]} ))`
`  `` (∀left,right:Form(C).  ({x:A| R[x;left]}  `` {x:A| R[x;right]}  `` {x:A| R[x;left ∨ right]} ))`
`  `` (∀body:Form(C). ({x:A| R[x;body]}  `` {x:A| R[x;¬(body)]} ))`
`  `` (∀var:Atom. ∀body:Form(C).  ({x:A| R[x;body]}  `` {x:A| R[x;∀var. body]} ))`
`  `` (∀var:Atom. ∀body:Form(C).  ({x:A| R[x;body]}  `` {x:A| R[x;∃var. body]} ))`
`  `` {∀v:Form(C). {x:A| R[x;v]} })`

Definition: Form_ind
`Form_ind(v;`
`         FormVar(name)`` Var[name];`
`         FormConst(value)`` Const[value];`
`         FormSet(var,phi)`` rec1.Set[var;`
`                                     phi;`
`                                     rec1];`
`         FormEqual(left,right)`` rec2,rec3.Equal[left;`
`                                                 right;`
`                                                 rec2;`
`                                                 rec3];`
`         FormMember(element,set)`` rec4,rec5.Member[element;`
`                                                    set;`
`                                                    rec4;`
`                                                    rec5];`
`         FormAnd(left,right)`` rec6,rec7.And[left;`
`                                             right;`
`                                             rec6;`
`                                             rec7];`
`         FormOr(left,right)`` rec8,rec9.Or[left;`
`                                           right;`
`                                           rec8;`
`                                           rec9];`
`         FormNot(body)`` rec10.Not[body; rec10];`
`         FormAll(var,body)`` rec11.All[var;`
`                                       body;`
`                                       rec11];`
`         FormExists(var,body)`` rec12.Exists[var;`
`                                             body;`
`                                             rec12])  ==`
`  fix((λForm_ind,v. let lbl,v1 = v `
`                    in if lbl="Var" then Var[v1]`
`                       if lbl="Const" then Const[v1]`
`                       if lbl="Set"`
`                         then let var,v2 = v1 `
`                              in Set[var;`
`                                     v2;`
`                                     Form_ind v2]`
`                       if lbl="Equal"`
`                         then let left,v2 = v1 `
`                              in Equal[left;`
`                                       v2;`
`                                       Form_ind left;`
`                                       Form_ind v2]`
`                       if lbl="Member"`
`                         then let element,v2 = v1 `
`                              in Member[element;`
`                                        v2;`
`                                        Form_ind element;`
`                                        Form_ind v2]`
`                       if lbl="And"`
`                         then let left,v2 = v1 `
`                              in And[left;`
`                                     v2;`
`                                     Form_ind left;`
`                                     Form_ind v2]`
`                       if lbl="Or"`
`                         then let left,v2 = v1 `
`                              in Or[left;`
`                                    v2;`
`                                    Form_ind left;`
`                                    Form_ind v2]`
`                       if lbl="Not" then Not[v1; Form_ind v1]`
`                       if lbl="All"`
`                         then let var,v2 = v1 `
`                              in All[var;`
`                                     v2;`
`                                     Form_ind v2]`
`                       if lbl="Exists"`
`                         then let var,v2 = v1 `
`                              in Exists[var;`
`                                        v2;`
`                                        Form_ind v2]`
`                       else Ax`
`                       fi )) `
`  v`

Lemma: Form_ind_wf
`∀[C,A:Type]. ∀[R:A ⟶ Form(C) ⟶ ℙ]. ∀[v:Form(C)]. ∀[Var:name:Atom ⟶ {x:A| R[x;Vname]} ].`
`∀[Const:value:C ⟶ {x:A| R[x;Const(value)]} ]. ∀[Set:var:Atom`
`                                                    ⟶ phi:Form(C)`
`                                                    ⟶ {x:A| R[x;phi]} `
`                                                    ⟶ {x:A| R[x;{var | phi}]} ]. ∀[Equal:left:Form(C)`
`                                                                                         ⟶ right:Form(C)`
`                                                                                         ⟶ {x:A| R[x;left]} `
`                                                                                         ⟶ {x:A| R[x;right]} `
`                                                                                         ⟶ {x:A| R[x;left = right]} ].`
`∀[Member:element:Form(C) ⟶ set:Form(C) ⟶ {x:A| R[x;element]}  ⟶ {x:A| R[x;set]}  ⟶ {x:A| R[x;element ∈ set]} ].`
`∀[And:left:Form(C) ⟶ right:Form(C) ⟶ {x:A| R[x;left]}  ⟶ {x:A| R[x;right]}  ⟶ {x:A| R[x;left ∧ right)]} ].`
`∀[Or:left:Form(C) ⟶ right:Form(C) ⟶ {x:A| R[x;left]}  ⟶ {x:A| R[x;right]}  ⟶ {x:A| R[x;left ∨ right]} ].`
`∀[Not:body:Form(C) ⟶ {x:A| R[x;body]}  ⟶ {x:A| R[x;¬(body)]} ]. ∀[All:var:Atom`
`                                                                      ⟶ body:Form(C)`
`                                                                      ⟶ {x:A| R[x;body]} `
`                                                                      ⟶ {x:A| R[x;∀var. body]} ].`
`∀[Exists:var:Atom ⟶ body:Form(C) ⟶ {x:A| R[x;body]}  ⟶ {x:A| R[x;∃var. body]} ].`
`  (Form_ind(v;`
`            FormVar(name)`` Var[name];`
`            FormConst(value)`` Const[value];`
`            FormSet(var,phi)`` rec1.Set[var;phi;rec1];`
`            FormEqual(left,right)`` rec2,rec3.Equal[left;right;rec2;rec3];`
`            FormMember(element,set)`` rec4,rec5.Member[element;set;rec4;rec5];`
`            FormAnd(left,right)`` rec6,rec7.And[left;right;rec6;rec7];`
`            FormOr(left,right)`` rec8,rec9.Or[left;right;rec8;rec9];`
`            FormNot(body)`` rec10.Not[body;rec10];`
`            FormAll(var,body)`` rec11.All[var;body;rec11];`
`            FormExists(var,body)`` rec12.Exists[var;body;rec12])  ∈ {x:A| R[x;v]} )`

Lemma: Form_ind_wf_simple
`∀[C,A:Type]. ∀[v:Form(C)]. ∀[Var:name:Atom ⟶ A]. ∀[Const:value:C ⟶ A]. ∀[Set:var:Atom ⟶ phi:Form(C) ⟶ A ⟶ A].`
`∀[Equal,Member,And,Or:left:Form(C) ⟶ right:Form(C) ⟶ A ⟶ A ⟶ A]. ∀[Not:body:Form(C) ⟶ A ⟶ A].`
`∀[All,Exists:var:Atom ⟶ body:Form(C) ⟶ A ⟶ A].`
`  (Form_ind(v;`
`            FormVar(name)`` Var[name];`
`            FormConst(value)`` Const[value];`
`            FormSet(var,phi)`` rec1.Set[var;phi;rec1];`
`            FormEqual(left,right)`` rec2,rec3.Equal[left;right;rec2;rec3];`
`            FormMember(element,set)`` rec4,rec5.Member[element;set;rec4;rec5];`
`            FormAnd(left,right)`` rec6,rec7.And[left;right;rec6;rec7];`
`            FormOr(left,right)`` rec8,rec9.Or[left;right;rec8;rec9];`
`            FormNot(body)`` rec10.Not[body;rec10];`
`            FormAll(var,body)`` rec11.All[var;body;rec11];`
`            FormExists(var,body)`` rec12.Exists[var;body;rec12])  ∈ A)`

Lemma: subtype_rel_Formco
`∀[A,B:Type].  Formco(A) ⊆r Formco(B) supposing A ⊆r B`

Lemma: subtype_rel_Form
`∀[A,B:Type].  Form(A) ⊆r Form(B) supposing A ⊆r B`

Definition: wfFormAux
`wfFormAux(f) ==`
`  Form_ind(f;`
`           FormVar(v)`` λisterm.isterm;`
`           FormConst(c)`` λisterm.isterm;`
`           FormSet(x,phi)`` r.λisterm.(isterm ∧b (r ff));`
`           FormEqual(l,r)`` r1,r2.λisterm.((¬bisterm) ∧b (r1 tt) ∧b (r2 tt));`
`           FormMember(e,s)`` r1,r2.λisterm.((¬bisterm) ∧b (r1 tt) ∧b (r2 tt));`
`           FormAnd(l,r)`` r1,r2.λisterm.((¬bisterm) ∧b (r1 ff) ∧b (r2 ff));`
`           FormOr(l,r)`` r1,r2.λisterm.((¬bisterm) ∧b (r1 ff) ∧b (r2 ff));`
`           FormNot(b)`` r1.λisterm.((¬bisterm) ∧b (r1 ff));`
`           FormAll(x,b)`` r1.λisterm.((¬bisterm) ∧b (r1 ff));`
`           FormExists(x,b)`` r1.λisterm.((¬bisterm) ∧b (r1 ff))) `

Lemma: wfFormAux_wf
`∀[c:Type]. ∀[f:Form(c)].  (wfFormAux(f) ∈ 𝔹 ⟶ 𝔹)`

Definition: termForm
`termForm(f) ==`
`  Form_ind(f;`
`           FormVar(v)`` tt;`
`           FormConst(c)`` tt;`
`           FormSet(x,phi)`` r.tt;`
`           FormEqual(l,r)`` a,b.ff;`
`           FormMember(e,s)`` a,b.ff;`
`           FormAnd(l,r)`` a,b.ff;`
`           FormOr(l,r)`` a,b.ff;`
`           FormNot(x)`` a.ff;`
`           FormAll(x,b)`` a.ff;`
`           FormExists(x,b)`` a.ff) `

Lemma: termForm_wf
`∀[c:Type]. ∀[f:Form(c)].  (termForm(f) ∈ 𝔹)`

Definition: wfForm
`wfForm(f) ==  wfFormAux(f) termForm(f)`

Lemma: wfForm_wf
`∀[C:Type]. ∀[f:Form(C)].  (wfForm(f) ∈ 𝔹)`

Lemma: wfFormAux-unique
`∀[C:Type]. ∀[f:Form(C)]. ∀[b:𝔹].  ((↑(wfFormAux(f) b)) `` termForm(f) = b)`

Definition: FormFvs
`FormFvs(f) ==`
`  Form_ind(f;`
`           FormVar(v)`` [v];`
`           FormConst(c)`` [];`
`           FormSet(x,phi)`` fvsphi.filter(λv.(¬bv =a x);fvsphi);`
`           FormEqual(t1,t2)`` fvs1,fvs2.fvs1 ⋃ fvs2;`
`           FormMember(t1,t2)`` fvs1,fvs2.fvs1 ⋃ fvs2;`
`           FormAnd(a,b)`` fvsa,fvsb.fvsa ⋃ fvsb;`
`           FormOr(a,b)`` fvsa,fvsb.fvsa ⋃ fvsb;`
`           FormNot(a)`` fvsa.fvsa;`
`           FormAll(x,phi)`` fvsphi.filter(λv.(¬bv =a x);fvsphi);`
`           FormExists(x,phi)`` fvsphi.filter(λv.(¬bv =a x);fvsphi)) `

Lemma: FormFvs_wf
`∀[c:Type]. ∀[f:Form(c)].  (FormFvs(f) ∈ Atom List)`

Definition: FormSafe1
`FormSafe1(f) ==`
`  Form_ind(f;`
`           FormVar(v)`` λvs.False;`
`           FormConst(c)`` λvs.False;`
`           FormSet(x,phi)`` r.λvs.False;`
`           FormEqual(a,b)`` ra,rb.λvs.((↑null(vs))`
`                                      ∨ (∃x:Atom`
`                                          (set-equal(Atom;vs;[x])`
`                                          ∧ (((↑FormVar?(a)) ∧ (FormVar-name(a) = x ∈ Atom) ∧ (¬(x ∈ FormFvs(b))))`
`                                            ∨ ((↑FormVar?(b)) ∧ (FormVar-name(b) = x ∈ Atom) ∧ (¬(x ∈ FormFvs(a))))))));`
`           FormMember(a,b)`` ra,rb.λvs.((↑null(vs))`
`                                       ∨ (∃x:Atom`
`                                           (set-equal(Atom;vs;[x])`
`                                           ∧ (↑FormVar?(a))`
`                                           ∧ (FormVar-name(a) = x ∈ Atom)`
`                                           ∧ (((↑FormVar?(b)) ∧ (FormVar-name(b) = x ∈ Atom)) ∨ (¬(x ∈ FormFvs(b)))))));`
`           FormAnd(a,b)`` ra,rb.λvs.∃as,bs:Atom List`
`                                     (set-equal(Atom;vs;as @ bs)`
`                                     ∧ (ra as)`
`                                     ∧ (rb bs)`
`                                     ∧ (l_disjoint(Atom;as;FormFvs(b)) ∨ l_disjoint(Atom;bs;FormFvs(a))));`
`           FormOr(a,b)`` ra,rb.λvs.((ra vs) ∧ (rb vs));`
`           FormNot(a)`` ra.λvs.((↑null(vs)) ∧ (ra []));`
`           FormAll(x,phi)`` r.λvs.False;`
`           FormExists(x,phi)`` r.λvs.((¬(x ∈ vs)) ∧ (r [x / vs]))) `

Lemma: FormSafe1_wf
`∀[C:Type]. ∀[f:Form(C)].  (FormSafe1(f) ∈ (Atom List) ⟶ ℙ)`

Lemma: FormSafe1_functionality
`∀C:Type. ∀phi:Form(C). ∀vs,ws:Atom List.  (l_subset(Atom;ws;vs) `` {(FormSafe1(phi) vs) `` (FormSafe1(phi) ws)})`

Lemma: FormSafe1-Fvs-subset
`∀C:Type. ∀phi:Form(C). ∀vs:Atom List.  ((FormSafe1(phi) vs) `` l_subset(Atom;vs;FormFvs(phi)))`

Definition: PZF-safe
`PZF-safe(phi;vs) ==  FormSafe1(phi) vs`

Lemma: PZF-safe_wf
`∀[C:Type]. ∀[phi:Form(C)]. ∀[vs:Atom List].  (PZF-safe(phi;vs) ∈ ℙ)`

Lemma: PZF-safe_functionality
`∀C:Type. ∀phi:Form(C). ∀vs,ws:Atom List.  (l_subset(Atom;ws;vs) `` {PZF-safe(phi;vs) `` PZF-safe(phi;ws)})`

Lemma: PZF-safe-Fvs-subset
`∀C:Type. ∀phi:Form(C). ∀vs:Atom List.  (PZF-safe(phi;vs) `` l_subset(Atom;vs;FormFvs(phi)))`

Definition: FormSafe1'
`FormSafe1'(f) ==`
`  Form_ind(f;`
`           FormVar(v)`` λvs.False;`
`           FormConst(c)`` λvs.False;`
`           FormSet(x,phi)`` r.λvs.False;`
`           FormEqual(a,b)`` ra,rb.λvs.((↑null(vs))`
`                                      ∨ (∃x:Atom`
`                                          (set-equal(Atom;vs;[x])`
`                                          ∧ (((↑FormVar?(a)) ∧ (FormVar-name(a) = x ∈ Atom) ∧ (¬(x ∈ FormFvs(b))))`
`                                            ∨ ((↑FormVar?(b)) ∧ (FormVar-name(b) = x ∈ Atom) ∧ (¬(x ∈ FormFvs(a))))))));`
`           FormMember(a,b)`` ra,rb.λvs.((↑null(vs))`
`                                       ∨ (∃x:Atom`
`                                           (set-equal(Atom;vs;[x])`
`                                           ∧ (↑FormVar?(a))`
`                                           ∧ (FormVar-name(a) = x ∈ Atom)`
`                                           ∧ (((↑FormVar?(b)) ∧ (FormVar-name(b) = x ∈ Atom)) ∨ (¬(x ∈ FormFvs(b)))))));`
`           FormAnd(a,b)`` ra,rb.λvs.((∃theta:Atom List`
`                                       (l_subset(Atom;theta;vs-FormFvs(b)) ∧ (ra theta) ∧ (rb vs-theta)))`
`                                    ∨ (∃phi:Atom List. (l_subset(Atom;phi;vs-FormFvs(a)) ∧ (ra vs-phi) ∧ (rb phi))));`
`           FormOr(a,b)`` ra,rb.λvs.((ra vs) ∧ (rb vs));`
`           FormNot(a)`` ra.λvs.((↑null(vs)) ∧ (ra []));`
`           FormAll(x,phi)`` r.λvs.False;`
`           FormExists(x,phi)`` r.λvs.((¬(x ∈ vs)) ∧ (r [x / vs]))) `

Lemma: FormSafe1'_wf
`∀[C:Type]. ∀[f:Form(C)].  (FormSafe1'(f) ∈ (Atom List) ⟶ ℙ)`

Lemma: FormSafe-iff-FormSafe1'
`∀C:Type. ∀f:Form(C). ∀vs:Atom List.  (FormSafe1(f) vs `⇐⇒` FormSafe1'(f) vs)`

Definition: FormSafe1''
`FormSafe1''(f) ==`
`  Form_ind(f;`
`           FormVar(v)`` λvs.False;`
`           FormConst(c)`` λvs.False;`
`           FormSet(x,phi)`` r.λvs.False;`
`           FormEqual(a,b)`` ra,rb.λvs.((↑null(vs))`
`                                      ∨ (∃x:Atom`
`                                          (set-equal(Atom;vs;[x])`
`                                          ∧ (((↑FormVar?(a)) ∧ (FormVar-name(a) = x ∈ Atom) ∧ (¬(x ∈ FormFvs(b))))`
`                                            ∨ ((↑FormVar?(b)) ∧ (FormVar-name(b) = x ∈ Atom) ∧ (¬(x ∈ FormFvs(a))))))));`
`           FormMember(a,b)`` ra,rb.λvs.((↑null(vs))`
`                                       ∨ (∃x:Atom`
`                                           (set-equal(Atom;vs;[x])`
`                                           ∧ (↑FormVar?(a))`
`                                           ∧ (FormVar-name(a) = x ∈ Atom)`
`                                           ∧ (((↑FormVar?(b)) ∧ (FormVar-name(b) = x ∈ Atom)) ∨ (¬(x ∈ FormFvs(b)))))));`
`           FormAnd(a,b)`` ra,rb.λvs.(let theta = vs-FormFvs(b) in`
`                                         (ra theta) ∧ (rb vs-theta)`
`                                    ∨ let phi = vs-FormFvs(a) in`
`                                          (ra vs-phi) ∧ (rb phi));`
`           FormOr(a,b)`` ra,rb.λvs.((ra vs) ∧ (rb vs));`
`           FormNot(a)`` ra.λvs.((↑null(vs)) ∧ (ra []));`
`           FormAll(x,phi)`` r.λvs.False;`
`           FormExists(x,phi)`` r.λvs.((¬(x ∈ vs)) ∧ (r [x / vs]))) `

Lemma: FormSafe1''_wf
`∀[C:Type]. ∀[f:Form(C)].  (FormSafe1''(f) ∈ (Atom List) ⟶ ℙ)`

Lemma: FormSafe1'-iff-FormSafe1''
`∀C:Type. ∀f:Form(C). ∀vs:Atom List.  (FormSafe1'(f) vs `⇐⇒` FormSafe1''(f) vs)`

Lemma: FormSafe1-iff-FormSafe1''
`∀C:Type. ∀f:Form(C). ∀vs:Atom List.  (FormSafe1(f) vs `⇐⇒` FormSafe1''(f) vs)`

Definition: FormSafe2
`FormSafe2(f) ==`
`  Form_ind(f;`
`           FormVar(v)`` λvs.ff;`
`           FormConst(c)`` λvs.ff;`
`           FormSet(x,phi)`` r.λvs.ff;`
`           FormEqual(a,b)`` ra,rb.λvs.(null(vs)`
`                                      ∨blet x = hd(vs) in`
`                                            null(vs-[x])`
`                                            ∧b ((FormVar?(a) ∧b FormVar-name(a) =a x ∧b (¬bx ∈b FormFvs(b)))`
`                                               ∨b(FormVar?(b) ∧b FormVar-name(b) =a x ∧b (¬bx ∈b FormFvs(a)))));`
`           FormMember(a,b)`` ra,rb.λvs.(null(vs)`
`                                       ∨blet x = hd(vs) in`
`                                             null(vs-[x])`
`                                             ∧b FormVar?(a)`
`                                             ∧b FormVar-name(a) =a x`
`                                             ∧b ((FormVar?(b) ∧b FormVar-name(b) =a x) ∨b(¬bx ∈b FormFvs(b))));`
`           FormAnd(a,b)`` ra,rb.λvs.eval as = FormFvs(a) in`
`                                    eval bs = FormFvs(b) in`
`                                      eval theta = vs-bs in`
`                                      (ra theta) ∧b (rb vs-theta)`
`                                      ∨beval phi = vs-as in`
`                                        (ra vs-phi) ∧b (rb phi);`
`           FormOr(a,b)`` ra,rb.λvs.((ra vs) ∧b (rb vs));`
`           FormNot(a)`` ra.λvs.(null(vs) ∧b (ra []));`
`           FormAll(x,phi)`` r.λvs.ff;`
`           FormExists(x,phi)`` r.λvs.((¬bx ∈b vs) ∧b (r [x / vs]))) `

Lemma: FormSafe2_wf
`∀[C:Type]. ∀[f:Form(C)].  (FormSafe2(f) ∈ (Atom List) ⟶ 𝔹)`

Definition: PZF_safe
`PZF_safe(phi;vs) ==  FormSafe2(phi) vs`

Lemma: PZF_safe_wf
`∀[C:Type]. ∀[phi:Form(C)]. ∀[vs:Atom List].  (PZF_safe(phi;vs) ∈ 𝔹)`

Lemma: PZF_safe_functionality
`∀[C:Type]. ∀[phi:Form(C)]. ∀[vs,ws:Atom List].  PZF_safe(phi;vs) = PZF_safe(phi;ws) supposing set-equal(Atom;vs;ws)`

Lemma: assert-PZF_safe
`∀C:Type. ∀phi:Form(C). ∀vs:Atom List.  (↑PZF_safe(phi;vs) `⇐⇒` PZF-safe(phi;vs))`

Lemma: PZF_safe_functionality_subset
`∀[C:Type]. ∀[phi:Form(C)]. ∀[vs,ws:Atom List].`
`  (↑PZF_safe(phi;vs)) `` (↑PZF_safe(phi;ws)) supposing l_subset(Atom;ws;vs)`

Definition: SafeForm
`SafeForm(f) ==`
`  Form_ind(f;`
`           FormVar(v)`` tt;`
`           FormConst(c)`` tt;`
`           FormSet(x,phi)`` r.r ∧b PZF_safe(phi;[x]);`
`           FormEqual(l,r)`` r1,r2.r1 ∧b r2;`
`           FormMember(e,s)`` r1,r2.r1 ∧b r2;`
`           FormAnd(l,r)`` r1,r2.r1 ∧b r2;`
`           FormOr(l,r)`` r1,r2.r1 ∧b r2;`
`           FormNot(b)`` r1.r1;`
`           FormAll(x,b)`` r1.r1;`
`           FormExists(x,b)`` r1.r1) `

Lemma: SafeForm_wf
`∀[C:Type]. ∀[f:Form(C)].  (SafeForm(f) ∈ 𝔹)`

Definition: PZF-Form
`PZF-Form(C) ==  {f:Form(C)| (↑wfForm(f)) ∧ (↑SafeForm(f))} `

Lemma: PZF-Form_wf
`∀[C:Type]. (PZF-Form(C) ∈ Type)`

Definition: PZF-Term
`PZF-Term(C) ==  {f:PZF-Form(C)| ↑termForm(f)} `

Lemma: PZF-Term_wf
`∀[C:Type]. (PZF-Term(C) ∈ Type)`

Definition: PZF-Formula
`PZF-Formula(C) ==  {f:PZF-Form(C)| ¬↑termForm(f)} `

Lemma: PZF-Formula_wf
`∀[C:Type]. (PZF-Formula(C) ∈ Type)`

Lemma: FormSet_wf2
`∀[C:Type]. ∀[x:Atom]. ∀[phi:PZF-Formula(C)].  {x | phi} ∈ PZF-Term(C) supposing PZF-safe(phi;[x])`

Lemma: FormEqual_wf2
`∀[C:Type]. ∀[a,b:PZF-Term(C)].  (a = b ∈ PZF-Formula(C))`

Lemma: FormMember_wf2
`∀[C:Type]. ∀[a,b:PZF-Term(C)].  (a ∈ b ∈ PZF-Formula(C))`

Lemma: FormAnd_wf2
`∀[C:Type]. ∀[a,b:PZF-Formula(C)].  (a ∧ b) ∈ PZF-Formula(C))`

Lemma: FormOr_wf2
`∀[C:Type]. ∀[a,b:PZF-Formula(C)].  (a ∨ b ∈ PZF-Formula(C))`

Lemma: FormNot_wf2
`∀[C:Type]. ∀[a:PZF-Formula(C)].  (¬(a) ∈ PZF-Formula(C))`

Lemma: FormAll_wf2
`∀[C:Type]. ∀[a:PZF-Formula(C)]. ∀[x:Atom].  (∀x. a ∈ PZF-Formula(C))`

Lemma: FormExists_wf2
`∀[C:Type]. ∀[a:PZF-Formula(C)]. ∀[x:Atom].  (∃x. a ∈ PZF-Formula(C))`

Lemma: PZF-induction
`∀C:Type`
`  ∀[F:PZF-Formula(C) ⟶ ℙ]. ∀[T:PZF-Term(C) ⟶ ℙ].`
`    ((∀name:Atom. T[Vname])`
`    `` (∀value:C. T[Const(value)])`
`    `` (∀x:Atom. ∀phi:PZF-Formula(C).  (F[phi] `` PZF-safe(phi;[x]) `` T[{x | phi}]))`
`    `` (∀a,b:PZF-Term(C).  (T[a] `` T[b] `` F[a = b]))`
`    `` (∀a,b:PZF-Term(C).  (T[a] `` T[b] `` F[a ∈ b]))`
`    `` (∀a,b:PZF-Formula(C).  (F[a] `` F[b] `` F[a ∧ b)]))`
`    `` (∀a,b:PZF-Formula(C).  (F[a] `` F[b] `` F[a ∨ b]))`
`    `` (∀a:PZF-Formula(C). (F[a] `` F[¬(a)]))`
`    `` (∀a:PZF-Formula(C). ∀x:Atom.  (F[a] `` F[∀x. a]))`
`    `` (∀a:PZF-Formula(C). ∀x:Atom.  (F[a] `` F[∃x. a]))`
`    `` ((∀phi:PZF-Formula(C). F[phi]) ∧ (∀t:PZF-Term(C). T[t])))`

Definition: validForm
`validForm(f) ==  wfForm(f) ∧b SafeForm(f)`

Lemma: validForm_wf
`∀[C:Type]. ∀[f:Form(C)].  (validForm(f) ∈ 𝔹)`

Home Index