---

Step * of Lemma PZF_safe_functionality_subset

∀[C:Type]. ∀[phi:Form(C)]. ∀[vs,ws:Atom List].
  (↑PZF_safe(phi;vs)) ⇒ (↑PZF_safe(phi;ws)) supposing l_subset(Atom;ws;vs)
BY
{ (Auto THEN (InstLemma `FormSafe1_functionality` [⌜C⌝;⌜phi⌝;⌜vs⌝;⌜ws⌝]⋅ THENA Auto)) }

1
1. C : Type
2. phi : Form(C)
3. vs : Atom List
4. ws : Atom List
5. l_subset(Atom;ws;vs)
6. ↑PZF_safe(phi;vs)
7. (FormSafe1(phi) vs) ⇒ (FormSafe1(phi) ws)
⊢ ↑PZF_safe(phi;ws)

---

Latex:

---

Latex:
\mforall{}[C:Type].  \mforall{}[phi:Form(C)].  \mforall{}[vs,ws:Atom  List].
    (\muparrow{}PZF\_safe(phi;vs))  {}\mRightarrow{}  (\muparrow{}PZF\_safe(phi;ws))  supposing  l\_subset(Atom;ws;vs)


By

---

Latex:
(Auto  THEN  (InstLemma  `FormSafe1\_functionality`  [\mkleeneopen{}C\mkleeneclose{};\mkleeneopen{}phi\mkleeneclose{};\mkleeneopen{}vs\mkleeneclose{};\mkleeneopen{}ws\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index