---

Step * of Lemma iff_imp_equal_bool

∀[a,b:𝔹].  a = b supposing ↑a ⇐⇒ ↑b
BY
{ (UnivCD THENA Auto) }

1
1. a : 𝔹
2. b : 𝔹
3. ↑a ⇐⇒ ↑b
⊢ a = b

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbB{}].    a  =  b  supposing  \muparrow{}a  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}b


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index