(8steps)
PrintForm
Definitions
list
3
jlc
Sections
Support(jlc)
Doc
At:
sublist
of
nil
iff
nil
1
1
1
1.
T:
Type
2.
eq:
{T=
}
3.
L:
T List
x
L.False
L = nil
By:
Analyze 3
THEN
Rewrite (HigherC list_all_unrollC) 0
Generated subgoals:
1
True
nil = nil
T List
2
4.
u:
T
5.
v:
T List
False &
x
v.False
u.v = nil
About:
(8steps)
PrintForm
Definitions
list
3
jlc
Sections
Support(jlc)
Doc
True 
nil = nil 
T List False & 
xv.False u.v = nil
}
xL.False L = nil
True nil = nil T List False & xv.False u.v = nil
