(4steps)
PrintForm
Definitions
list
3
jlc
Sections
Support(jlc)
Doc
At:
sublist
wf
1
2
1.
T:
Type
2.
eq:
T
T
3.
L1:
T List
4.
L2:
T List
5.
u:
T
6.
v:
T List
7.
v(
eq)L2
Type
(u.v)(
eq)L2
Type
By:
AbReduce 0
Generated subgoals:
None
About:
(4steps)
PrintForm
Definitions
list
3
jlc
Sections
Support(jlc)
Doc