---

Step * of Lemma PZF-safe-Fvs-subset

∀C:Type. ∀phi:Form(C). ∀vs:Atom List.  (PZF-safe(phi;vs) ⇒ l_subset(Atom;vs;FormFvs(phi)))
BY
{ (InstLemma `FormSafe1-Fvs-subset` [] THEN RepeatFor 4 (ParallelLast') THEN Auto) }

---

Latex:

---

Latex:
\mforall{}C:Type.  \mforall{}phi:Form(C).  \mforall{}vs:Atom  List.    (PZF-safe(phi;vs)  {}\mRightarrow{}  l\_subset(Atom;vs;FormFvs(phi)))


By

---

Latex:
(InstLemma  `FormSafe1-Fvs-subset`  []  THEN  RepeatFor  4  (ParallelLast')  THEN  Auto)

---

Home Index