---

Step * of Lemma co-list-cases

∀[T:Type]
  ∀x:colist(T)
    (((↑isaxiom(x)) ∧ (x = Ax ∈ Unit)) ∨ ((↑ispair(x)) ∧ (∃t:T. ∃y:colist(T). (x = <t, y> ∈ (T × colist(T))))))
BY
{ (Auto
   THEN GenConcl ⌜x = c ∈ (Unit ⋃ (T × colist(T)))⌝⋅
   THEN (Auto THEN ThinVar `x')
   THEN UseWitness ⌜if c = Ax then inl <Ax, Ax> otherwise let t,y = c 
                                       in inr <Ax, t, y, Ax> ⌝⋅
   THEN D_b_union (-1)⋅
   THEN Try ((BLemma `unit-product-disjoint` THEN Auto))
   THEN GenConclAtAddr [2;1]
   THEN D -2
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  GenConcl  \mkleeneopen{}x  =  c\mkleeneclose{}\mcdot{}
  THEN  (Auto  THEN  ThinVar  `x')
  THEN  UseWitness  \mkleeneopen{}if  c  =  Ax  then  inl  <Ax,  Ax>  otherwise  let  t,y  =  c 
                                                                          in  inr  <Ax,  t,  y,  Ax>  \mkleeneclose{}\mcdot{}
  THEN  D\_b\_union  (-1)\mcdot{}
  THEN  Try  ((BLemma  `unit-product-disjoint`  THEN  Auto))
  THEN  GenConclAtAddr  [2;1]
  THEN  D  -2
  THEN  Reduce  0
  THEN  Auto)

---

Home Index