---

Step * 1 of Lemma FormExists_wf2


1. C : Type
2. a : Form(C)
3. ↑wfForm(a)
4. ↑SafeForm(a)
5. ¬↑termForm(a)
6. x : Atom
⊢ ↑wfForm(∃x. a)
BY
{ ((RepUR ``wfForm termForm wfFormAux`` 0 THEN Fold `wfFormAux` 0) THEN RW assert_pushdownC 0 THEN Auto) }

1
1. C : Type
2. a : Form(C)
3. ↑wfForm(a)
4. ↑SafeForm(a)
5. ¬↑termForm(a)
6. x : Atom
⊢ ↑(wfFormAux(a) ff)

---

Latex:

---

Latex:

1.  C  :  Type
2.  a  :  Form(C)
3.  \muparrow{}wfForm(a)
4.  \muparrow{}SafeForm(a)
5.  \mneg{}\muparrow{}termForm(a)
6.  x  :  Atom
\mvdash{}  \muparrow{}wfForm(\mexists{}x.  a)


By

---

Latex:
((RepUR  ``wfForm  termForm  wfFormAux``  0  THEN  Fold  `wfFormAux`  0)
  THEN  RW  assert\_pushdownC  0
  THEN  Auto)

---

Home Index