---

Step * 1 of Lemma iff_imp_equal_bool


1. a : 𝔹
2. b : 𝔹
3. ↑a ⇐⇒ ↑b
⊢ a = b
BY
{ ((BoolCases 2 THEN BoolCases 1) THEN RWH assert_evalC (-1) THEN Auto) }

1
1. False ⇒ True
2. False ⇐ True
⊢ ff = tt

---

Latex:

---

Latex:

1.  a  :  \mBbbB{}
2.  b  :  \mBbbB{}
3.  \muparrow{}a  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}b
\mvdash{}  a  =  b


By

---

Latex:
((BoolCases  2  THEN  BoolCases  1)  THEN  RWH  assert\_evalC  (-1)  THEN  Auto)

---

Home Index