---

Step * of Lemma cocons_wf

∀[A:Type]. ∀[a:A]. ∀[L:co-list-islist(A)].  (cocons(a;L) ∈ co-list-islist(A))
BY
{ ((InstLemma `colist-ext` []⋅ THEN ParallelLast')
   THEN (Auto THEN DVar `L')
   THEN Unfolds ``cocons co-list-islist`` 0
   THEN At Type MemTypeCD⋅
   THEN Try (BLemma `has-value-is-list-of-co-list`)
   THEN Auto
   THEN SubsumeC ⌜Unit ⋃ (A × colist(A))⌝⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[a:A].  \mforall{}[L:co-list-islist(A)].    (cocons(a;L)  \mmember{}  co-list-islist(A))


By

---

Latex:
((InstLemma  `colist-ext`  []\mcdot{}  THEN  ParallelLast')
  THEN  (Auto  THEN  DVar  `L')
  THEN  Unfolds  ``cocons  co-list-islist``  0
  THEN  At  Type  MemTypeCD\mcdot{}
  THEN  Try  (BLemma  `has-value-is-list-of-co-list`)
  THEN  Auto
  THEN  SubsumeC  \mkleeneopen{}Unit  \mcup{}  (A  \mtimes{}  colist(A))\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index