---

Step * of Lemma bimplies_weakening

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

---

Latex:

---

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


By

---

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

---

Home Index