Step
*
1
1
2
1
of Lemma
list-cases
1. [T] : Type
2. x : colist(T)
3. [%1] : (colength(x))↓
4. x ∈ T × colist(T)
⊢ x ∈ T × (T List)
BY
{ TACTIC:Unhide }
1
1. T : Type
2. x : colist(T)
3. (colength(x))↓
4. x ∈ T × colist(T)
⊢ x ∈ T × (T List)
Latex:
Latex:
1. [T] : Type
2. x : colist(T)
3. [\%1] : (colength(x))\mdownarrow{}
4. x \mmember{} T \mtimes{} colist(T)
\mvdash{} x \mmember{} T \mtimes{} (T List)
By
Latex:
TACTIC:Unhide
Home
Index