---

Step * of Lemma co-list-ext

∀[T:Type]. colist(T) ≡ Unit ⋃ (T × colist(T))
BY
{ (Auto
   THEN Unfold `colist` 0
   THEN BLemma  `corec-ext`
   THEN Auto
   THEN D 0
   THEN Auto
   THEN BLemma `strong-continuous-b-union`
   THEN Auto
   THEN Try ((ProveContinuous THEN Auto)⋅)) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  colist(T)  \mequiv{}  Unit  \mcup{}  (T  \mtimes{}  colist(T))


By

---

Latex:
(Auto
  THEN  Unfold  `colist`  0
  THEN  BLemma    `corec-ext`
  THEN  Auto
  THEN  D  0
  THEN  Auto
  THEN  BLemma  `strong-continuous-b-union`
  THEN  Auto
  THEN  Try  ((ProveContinuous  THEN  Auto)\mcdot{}))

---

Home Index