(4steps)
PrintForm
Definitions
list
3
jlc
Sections
Support(jlc)
Doc
At:
sublist
wf1
1
1
1.
T:
Type
2.
eq:
{T=
}
3.
L1:
T List
4.
L2:
T List
nil(
eq)L2
Type
By:
Rewrite (HigherC sublist_unrollC) 0
Generated subgoals:
None
About:
(4steps)
PrintForm
Definitions
list
3
jlc
Sections
Support(jlc)
Doc