(12steps)
PrintForm
Definitions
Lemmas
list
3
jlc
Sections
Support(jlc)
Doc
At:
sublist
tail
T:Type. Discrete{T}
(
eq:{T
}, u:T, v:T List. v(
eq)(u.v))
By:
UnivCD
Generated subgoal:
1
1.
T:
Type
2.
Discrete{T}
3.
eq:
{T
}
4.
u:
T
5.
v:
T List
v(
eq)(u.v)
About:
(12steps)
PrintForm
Definitions
Lemmas
list
3
jlc
Sections
Support(jlc)
Doc
}
v(
eq)(u.v)
T:Type. Discrete{T} 
(eq:{T}, u:T, v:T List. v(eq)(u.v))
} v(eq)(u.v)
