---

Step * 1 of Lemma band-idempotent


1. b : 𝔹
⊢ b ∧b tt ~ b
BY
{ (Auto THEN RW (BoolSimpC) 0 THEN Auto) }

---

Latex:

---

Latex:

1.  b  :  \mBbbB{}
\mvdash{}  b  \mwedge{}\msubb{}  tt  \msim{}  b


By

---

Latex:
(Auto  THEN  RW  (BoolSimpC)  0  THEN  Auto)

---

Home Index