---

Step * of Lemma bool-cardinality-le

No Annotations
|𝔹| ≤ 2
BY
{ (((InstLemma `list-cardinality-le` [⌜𝔹⌝; ⌜[tt; ff]⌝])⋅ THENM Auto) THENW Auto) }

1
.....antecedent..... 
∀x:𝔹. (x ∈ [tt; ff])

---

Latex:

---

Latex:
No  Annotations
|\mBbbB{}|  \mleq{}  2


By

---

Latex:
(((InstLemma  `list-cardinality-le`  [\mkleeneopen{}\mBbbB{}\mkleeneclose{};  \mkleeneopen{}[tt;  ff]\mkleeneclose{}])\mcdot{}  THENM  Auto)  THENW  Auto)

---

Home Index