---

Step * of Lemma bool-tt-or-ff

∀b:𝔹. (b = tt ∨ b = ff)
BY
{ (Auto THEN AutoBoolCase ⌜b⌝⋅) }

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  AutoBoolCase  \mkleeneopen{}b\mkleeneclose{}\mcdot{})

---

Home Index