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