---

Step * of Lemma ispair-bool-if-co-list

∀[T:Type]. ∀[t:colist(T)].  (ispair(t) ∈ 𝔹)
BY
{ (InstLemma `colist-ext` [] THEN ParallelLast') }

1
1. [T] : Type
2. colist(T) ≡ Unit ⋃ (T × colist(T))
⊢ ∀[t:colist(T)]. (ispair(t) ∈ 𝔹)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[t:colist(T)].    (ispair(t)  \mmember{}  \mBbbB{})


By

---

Latex:
(InstLemma  `colist-ext`  []  THEN  ParallelLast')

---

Home Index