---

Step * of Lemma co-list-cases2

No Annotations
∀[T:Type]. ∀x:colist(T). ((x = Ax ∈ colist(T)) ∨ (∃t:T. ∃y:colist(T). (x = <t, y> ∈ colist(T))))
BY
{ ((Auto THEN (InstLemma `colist-ext` [⌜T⌝]⋅ THENA Auto) THEN D -1)
   THEN (Assert (T × colist(T)) ⊆r colist(T) BY
               ((D 0 THENA Auto) THEN SubsumeC ⌜Unit ⋃ (T × colist(T))⌝ ⋅ THEN Auto))
   THEN GenConcl ⌜x = c ∈ (Unit ⋃ (T × colist(T)))⌝⋅
   THEN (Auto THEN ThinVar `x')
   THEN UseWitness ⌜if c = Ax then inl Ax otherwise let t,y = c 
                                                    in inr <t, y, Ax> ⌝⋅
   THEN D_b_union (-1)⋅
   THEN D -1
   THEN Reduce 0
   THEN Auto
   THEN Try (Fold `it` 0)⋅
   THEN Try ((SubsumeC Unit ⋃ (T × colist(T))⋅ THEN Complete (Auto)))) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}x:colist(T).  ((x  =  Ax)  \mvee{}  (\mexists{}t:T.  \mexists{}y:colist(T).  (x  =  <t,  y>)))


By

---

Latex:
((Auto  THEN  (InstLemma  `colist-ext`  [\mkleeneopen{}T\mkleeneclose{}]\mcdot{}  THENA  Auto)  THEN  D  -1)
  THEN  (Assert  (T  \mtimes{}  colist(T))  \msubseteq{}r  colist(T)  BY
                          ((D  0  THENA  Auto)  THEN  SubsumeC  \mkleeneopen{}Unit  \mcup{}  (T  \mtimes{}  colist(T))\mkleeneclose{}  \mcdot{}  THEN  Auto))
  THEN  GenConcl  \mkleeneopen{}x  =  c\mkleeneclose{}\mcdot{}
  THEN  (Auto  THEN  ThinVar  `x')
  THEN  UseWitness  \mkleeneopen{}if  c  =  Ax  then  inl  Ax  otherwise  let  t,y  =  c 
                                                                                                    in  inr  <t,  y,  Ax>  \mkleeneclose{}\mcdot{}
  THEN  D\_b\_union  (-1)\mcdot{}
  THEN  D  -1
  THEN  Reduce  0
  THEN  Auto
  THEN  Try  (Fold  `it`  0)\mcdot{}
  THEN  Try  ((SubsumeC  Unit  \mcup{}  (T  \mtimes{}  colist(T))\mcdot{}  THEN  Complete  (Auto))))

---

Home Index