---

Step * of Lemma uiff_weakening

∀[P:ℙ]. (SqStable(P) ⇒ {uiff(P;P)})
BY
{ (Unfold `guard` 0 THEN (Auto THEN Unhide THEN Auto)) }

---

Latex:

---

Latex:
\mforall{}[P:\mBbbP{}].  (SqStable(P)  {}\mRightarrow{}  \{uiff(P;P)\})


By

---

Latex:
(Unfold  `guard`  0  THEN  (Auto  THEN  Unhide  THEN  Auto))

---

Home Index