---

Step * 1 1 of Lemma FormNot_wf2


1. C : Type
2. a : Form(C)
3. ↑wfForm(a)
4. ↑SafeForm(a)
5. ¬↑termForm(a)
⊢ ↑(wfFormAux(a) ff)
BY
{ ((NthHypEq 3 THEN EqCDA) THEN Unfold `wfForm` 0 THEN EqCDA THEN Auto) }

---

Latex:

---

Latex:

1.  C  :  Type
2.  a  :  Form(C)
3.  \muparrow{}wfForm(a)
4.  \muparrow{}SafeForm(a)
5.  \mneg{}\muparrow{}termForm(a)
\mvdash{}  \muparrow{}(wfFormAux(a)  ff)


By

---

Latex:
((NthHypEq  3  THEN  EqCDA)  THEN  Unfold  `wfForm`  0  THEN  EqCDA  THEN  Auto)

---

Home Index