---

Step * of Lemma assert_of_bimplies

∀[p:𝔹]. ∀[q:𝔹 supposing ↑p].  uiff(↑(p ⇒b q);↑q supposing ↑p)
BY
{ (Auto THEN BoolInd 1 THEN All Reduce THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[p:\mBbbB{}].  \mforall{}[q:\mBbbB{}  supposing  \muparrow{}p].    uiff(\muparrow{}(p  {}\mRightarrow{}\msubb{}  q);\muparrow{}q  supposing  \muparrow{}p)


By

---

Latex:
(Auto  THEN  BoolInd  1  THEN  All  Reduce  THEN  Auto)

---

Home Index