Nuprl - Proof: cons neq nil 1

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

1. T : Type
2. h : T
3. t : T List
4. h.t = nil

False

By:	ApFunToHypEquands `xs' (Case of xs; nil 0 ; y.ys 1) 4

Generated subgoal:

1 5. (Case of h.t; nil 0 ; y.ys 1) = (Case of nil; nil 0 ; y.ys 1)
False
1 step

About:

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