---

Step * 1 of Lemma list-cases


1. [T] : Type
2. x : T List
⊢ (x ~ []) ∨ (x ∈ T × (T List))
BY
{ TACTIC:(D -1 THEN (InstLemma `colist-cases` [⌜T⌝;⌜x⌝]⋅ THENA Auto)) }

1
1. [T] : Type
2. x : colist(T)
3. [%1] : (colength(x))↓
4. (x ~ Ax) ∨ (x ∈ T × colist(T))
⊢ (x ~ []) ∨ (x ∈ T × (T List))

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  x  :  T  List
\mvdash{}  (x  \msim{}  [])  \mvee{}  (x  \mmember{}  T  \mtimes{}  (T  List))


By

---

Latex:
TACTIC:(D  -1  THEN  (InstLemma  `colist-cases`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index