(4steps)
PrintForm
Definitions
list
3
jlc
Sections
Support(jlc)
Doc
At:
sublist
wf
T:Type, eq:(T
T
), L1,L2:T List. L1(
eq)L2
Type
By:
UnivCD
Generated subgoal:
1
1.
T:
Type
2.
eq:
T
T
3.
L1:
T List
4.
L2:
T List
L1(
eq)L2
Type
About:
(4steps)
PrintForm
Definitions
list
3
jlc
Sections
Support(jlc)
Doc