---

Step * of Lemma formula_ind_wf_simple

No Annotations
∀[A:Type]. ∀[v:formula()]. ∀[var:name:Atom ⟶ A]. ∀[not:sub:formula() ⟶ A ⟶ A]. ∀[and,or,imp:left:formula()
                                                                                               ⟶ right:formula()
                                                                                               ⟶ A
                                                                                               ⟶ A
                                                                                               ⟶ A].
  (formula_ind(v;
               pvar(name)⇒ var[name];
               pnot(sub)⇒ rec1.not[sub;rec1];
               pand(left,right)⇒ rec2,rec3.and[left;right;rec2;rec3];
               por(left,right)⇒ rec4,rec5.or[left;right;rec4;rec5];
               pimp(left,right)⇒ rec6,rec7.imp[left;right;rec6;rec7])  ∈ A)
BY
{ (ProveDatatypeIndWfSimple' formula_ind_wf) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A:Type].  \mforall{}[v:formula()].  \mforall{}[var:name:Atom  {}\mrightarrow{}  A].  \mforall{}[not:sub:formula()  {}\mrightarrow{}  A  {}\mrightarrow{}  A].
\mforall{}[and,or,imp:left:formula()  {}\mrightarrow{}  right:formula()  {}\mrightarrow{}  A  {}\mrightarrow{}  A  {}\mrightarrow{}  A].
    (formula\_ind(v;
                              pvar(name){}\mRightarrow{}  var[name];
                              pnot(sub){}\mRightarrow{}  rec1.not[sub;rec1];
                              pand(left,right){}\mRightarrow{}  rec2,rec3.and[left;right;rec2;rec3];
                              por(left,right){}\mRightarrow{}  rec4,rec5.or[left;right;rec4;rec5];
                              pimp(left,right){}\mRightarrow{}  rec6,rec7.imp[left;right;rec6;rec7])    \mmember{}  A)


By

---

Latex:
(ProveDatatypeIndWfSimple'  formula\_ind\_wf)

---

Home Index