---

Step * of Lemma bimplies_wf

∀[p:𝔹]. ∀[q:𝔹 supposing ↑p].  (p ⇒b q ∈ 𝔹)
BY
{ ((Auto THEN BoolInd 1) THEN Unfold `bimplies` 0 THEN All Reduce THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((Auto  THEN  BoolInd  1)  THEN  Unfold  `bimplies`  0  THEN  All  Reduce  THEN  Auto)

---

Home Index