---

Step * of Lemma PZF-safe_functionality

∀C:Type. ∀phi:Form(C). ∀vs,ws:Atom List.  (l_subset(Atom;ws;vs) ⇒ {PZF-safe(phi;vs) ⇒ PZF-safe(phi;ws)})
BY
{ (InstLemma `FormSafe1_functionality` []
   THEN RepeatFor 4 (ParallelLast')
   THEN All (Unfolds ``guard PZF-safe``)
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(InstLemma  `FormSafe1\_functionality`  []
  THEN  RepeatFor  4  (ParallelLast')
  THEN  All  (Unfolds  ``guard  PZF-safe``)
  THEN  Auto)

---

Home Index