---

Step * of Lemma colist-cases

∀[T:Type]. ∀x:colist(T). ((x ~ Ax) ∨ (x ∈ T × colist(T)))
BY
{ TACTIC:(InstLemma `colist-ext` []
          THEN ParallelLast'
          THEN D -1
          THEN (D 0 THENA Auto)
          THEN UseWitness ⌜isaxiom(x)⌝⋅
          THEN (SubsumeHyp ⌜Unit ⋃ (T × colist(T))⌝ (-1)⋅ THENA Auto)
          THEN D_b_union (-1)
          THEN D -1
          THEN RepUR ``btrue bfalse it`` 0
          THEN MemCD
          THEN Try (Complete (Auto))) }

1
.....eq aux..... 
1. T : Type
2. colist(T) ⊆r (Unit ⋃ (T × colist(T)))
3. (Unit ⋃ (T × colist(T))) ⊆r colist(T)
4. a2 : T
5. a3 : colist(T)
⊢ istype(<a2, a3> ~ Ax)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}x:colist(T).  ((x  \msim{}  Ax)  \mvee{}  (x  \mmember{}  T  \mtimes{}  colist(T)))


By

---

Latex:
TACTIC:(InstLemma  `colist-ext`  []
                THEN  ParallelLast'
                THEN  D  -1
                THEN  (D  0  THENA  Auto)
                THEN  UseWitness  \mkleeneopen{}isaxiom(x)\mkleeneclose{}\mcdot{}
                THEN  (SubsumeHyp  \mkleeneopen{}Unit  \mcup{}  (T  \mtimes{}  colist(T))\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
                THEN  D\_b\_union  (-1)
                THEN  D  -1
                THEN  RepUR  ``btrue  bfalse  it``  0
                THEN  MemCD
                THEN  Try  (Complete  (Auto)))

---

Home Index