Nuprl - Pf null true lemma 1 2 2

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

At: null true lemma 1 2 2

1. T: Type
2. L: T List
3. u: T
4. v: T List
5. u.v = nil

false = true

By: ApFunToHypEquands `x' (Case of x; nil 0 ; h.t 1) -1 THEN AbReduce -1

Generated subgoals:

None

About:

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