Nuprl - Proof: append is nil 1 1

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

1. T : Type
2. x : T
3. l : T List
4. [x / l] = nil
5. ||[x / l]|| = ||nil||

False

By:

Reduce -1

Generated subgoal:

1 5. ||l||+1 = 0
False
Auto

About:

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