---

Step * of Lemma bool_cases_sqequal

∀b:𝔹. ((b ~ tt) ∨ (b ~ ff))
BY
{ (Auto THEN RepeatFor 2 (D -1) THEN Fold `it` 0 THEN Folds ``btrue bfalse`` 0) }

1
1. x : 0 = 0 ∈ ℤ
⊢ (tt ~ tt) ∨ (tt ~ ff)

2
1. y : 0 = 0 ∈ ℤ
⊢ (ff ~ tt) ∨ (ff ~ ff)

---

Latex:

---

Latex:
\mforall{}b:\mBbbB{}.  ((b  \msim{}  tt)  \mvee{}  (b  \msim{}  ff))


By

---

Latex:
(Auto  THEN  RepeatFor  2  (D  -1)  THEN  Fold  `it`  0  THEN  Folds  ``btrue  bfalse``  0)

---

Home Index