(8steps)
PrintForm
Definitions
list
3
jlc
Sections
Support(jlc)
Doc
At:
sublist
of
nil
iff
nil
1
1.
T:
Type
2.
eq:
{T=
}
3.
L:
T List
L(
eq)nil
L = nil
By:
Unfold `sublist` 0
Generated subgoal:
1
x
L.x(
eq) nil
L = nil
About:
(8steps)
PrintForm
Definitions
list
3
jlc
Sections
Support(jlc)
Doc
x
L.x(eq) nil 
L = nil
}
L(
eq)nil L = nil
xL.x(eq) nil L = nil
