---

Step * of Lemma FormNot_wf2

∀[C:Type]. ∀[a:PZF-Formula(C)].  (¬(a) ∈ PZF-Formula(C))
BY
{ (Auto THEN RepeatFor 2 (D 2) THEN RepeatFor 2 ((MemTypeCD THEN Auto))) }

1
1. C : Type
2. a : Form(C)
3. ↑wfForm(a)
4. ↑SafeForm(a)
5. ¬↑termForm(a)
⊢ ↑wfForm(¬(a))

---

Latex:

---

Latex:
\mforall{}[C:Type].  \mforall{}[a:PZF-Formula(C)].    (\mneg{}(a)  \mmember{}  PZF-Formula(C))


By

---

Latex:
(Auto  THEN  RepeatFor  2  (D  2)  THEN  RepeatFor  2  ((MemTypeCD  THEN  Auto)))

---

Home Index