(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
23. u: T
4. v: T List
false = true u.v = nil

About:
listconsnilboolbfalsebtrueuniverseequal

(6steps) PrintForm Definitions list 3 jlc Sections Support(jlc) Doc