(6steps)
PrintForm
Definitions
list
3
jlc
Sections
Support(jlc)
Doc
At:
null
true
lemma
1
1.
T:
Type
2.
L:
T List
null(L) = true
L = nil
By:
Analyze -1
THEN
Rewrite (HigherC null_unrollC) 0
Generated subgoals:
1
true
= true
nil = nil
T List
2
3.
u:
T
4.
v:
T List
false
= true
u.v = nil
About:
(6steps)
PrintForm
Definitions
list
3
jlc
Sections
Support(jlc)
Doc
true
= true 
nil = nil 
T List false = true u.v = nil
null(L) = true L = nil
true = true nil = nil T List false = true u.v = nil
