---

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


1. [T] : Type
2. colist(T) ≡ Unit ⋃ (T × colist(T))
⊢ ∀[t:colist(T)]. (ispair(t) ∈ 𝔹)
BY
{ ((UnivCD THENA Auto) THEN CoListD (-1) THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  colist(T)  \mequiv{}  Unit  \mcup{}  (T  \mtimes{}  colist(T))
\mvdash{}  \mforall{}[t:colist(T)].  (ispair(t)  \mmember{}  \mBbbB{})


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  CoListD  (-1)  THEN  Reduce  0  THEN  Auto)

---

Home Index