Nuprl - Pf null false lemma 1

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

1. T: Type
2. L: T List

null(L) = false (h:T, t:T List. L = h.t)

By: Analyze -1 THEN Rewrite (HigherC null_unrollC) 0

Generated subgoals:

1 3. true = false
h:T, t:T List. nil = h.t

2 3. h:T, t:T List. nil = h.t
true = false

3 3. u: T
4. v: T List
5. false = false
h:T, t:T List. u.v = h.t

About:

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

1	3. `true = false` `h:T, t:T List. nil = h.t`
2	3. `h:T, t:T List. nil = h.t` `true = false`
3	3. `u:` `T` 4. `v:` `T List` 5. `false = false` `h:T, t:T List. u.v = h.t`