---

Step * 1 of Lemma colist-cases

.....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)
BY
{ ((Assert <a2, a3> ~ Ax ∈ Type BY (TACTIC:BLemma `pair-sq-axiom-wf` THEN Auto)) THEN Auto) }

---

Latex:

---

Latex:
.....eq  aux..... 
1.  T  :  Type
2.  colist(T)  \msubseteq{}r  (Unit  \mcup{}  (T  \mtimes{}  colist(T)))
3.  (Unit  \mcup{}  (T  \mtimes{}  colist(T)))  \msubseteq{}r  colist(T)
4.  a2  :  T
5.  a3  :  colist(T)
\mvdash{}  istype(<a2,  a3>  \msim{}  Ax)


By

---

Latex:
((Assert  <a2,  a3>  \msim{}  Ax  \mmember{}  Type  BY  (TACTIC:BLemma  `pair-sq-axiom-wf`  THEN  Auto))  THEN  Auto)

---

Home Index