---

Step * of Lemma FormSafe1-iff-FormSafe1''

∀C:Type. ∀f:Form(C). ∀vs:Atom List.  (FormSafe1(f) vs ⇐⇒ FormSafe1''(f) vs)
BY
{ ((RWO "FormSafe-iff-FormSafe1\'" 0 THENA Auto) THEN RWO "FormSafe1\'-iff-FormSafe1\'\'" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}C:Type.  \mforall{}f:Form(C).  \mforall{}vs:Atom  List.    (FormSafe1(f)  vs  \mLeftarrow{}{}\mRightarrow{}  FormSafe1''(f)  vs)


By

---

Latex:
((RWO  "FormSafe-iff-FormSafe1\mbackslash{}'"  0  THENA  Auto)  THEN  RWO  "FormSafe1\mbackslash{}'-iff-FormSafe1\mbackslash{}'\mbackslash{}'"  0  THEN  Auto)

---

Home Index