---

Step * 2 of Lemma FormOr_wf2


1. C : Type
2. a : Form(C)
3. ↑wfForm(a)
4. ↑SafeForm(a)
5. ¬↑termForm(a)
6. b : Form(C)
7. ↑wfForm(b)
8. ↑SafeForm(b)
9. ¬↑termForm(b)
10. ↑wfForm(a ∨ b)
⊢ ↑SafeForm(a ∨ b)
BY
{ ((RepUR ``SafeForm`` 0 THEN Fold `SafeForm` 0) THEN Auto) }

---

Latex:

---

Latex:

1.  C  :  Type
2.  a  :  Form(C)
3.  \muparrow{}wfForm(a)
4.  \muparrow{}SafeForm(a)
5.  \mneg{}\muparrow{}termForm(a)
6.  b  :  Form(C)
7.  \muparrow{}wfForm(b)
8.  \muparrow{}SafeForm(b)
9.  \mneg{}\muparrow{}termForm(b)
10.  \muparrow{}wfForm(a  \mvee{}  b)
\mvdash{}  \muparrow{}SafeForm(a  \mvee{}  b)


By

---

Latex:
((RepUR  ``SafeForm``  0  THEN  Fold  `SafeForm`  0)  THEN  Auto)

---

Home Index