---

Step * of Lemma assert_functionality_wrt_bimplies

∀[u,v:𝔹].  {↑v supposing ↑u} supposing ↑(u ⇒b v)
BY
{ (Unfold `guard` 0 THEN Unfold `bimplies` 0 THEN (D 0 THENA Auto) THEN AutoBoolCase ⌜u⌝⋅) }

---

Latex:

---

Latex:
\mforall{}[u,v:\mBbbB{}].    \{\muparrow{}v  supposing  \muparrow{}u\}  supposing  \muparrow{}(u  {}\mRightarrow{}\msubb{}  v)


By

---

Latex:
(Unfold  `guard`  0  THEN  Unfold  `bimplies`  0  THEN  (D  0  THENA  Auto)  THEN  AutoBoolCase  \mkleeneopen{}u\mkleeneclose{}\mcdot{})

---

Home Index