Nuprl - Proof: cons neq nil 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: cons neq nil 1 1

1. T : Type
2. h : T
3. t : T List
4. h.t = nil
5. (Case of h.t; nil

0 ; y.ys

1) = (Case of nil; nil

0 ; y.ys

False

By:

Reduce 5

Generated subgoals:

None

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html