---

Step * 1 of Lemma bool-cardinality-le

.....antecedent..... 
∀x:𝔹. (x ∈ [tt; ff])
BY
{ ((D 0 THENA Auto) THEN AutoBoolCase ⌜x⌝⋅) }

---

Latex:

---

Latex:
.....antecedent..... 
\mforall{}x:\mBbbB{}.  (x  \mmember{}  [tt;  ff])


By

---

Latex:
((D  0  THENA  Auto)  THEN  AutoBoolCase  \mkleeneopen{}x\mkleeneclose{}\mcdot{})

---

Home Index