Nuprl - Proof: pos length 2 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: pos length 2 1

1. A : Type
2. A List
3. u : A
4. v : A List
5.

u.v = nil

||v||+1

By:	Inst Thm* l:A List. \|\|l\|\|0 [A;v]

Generated subgoals:

None

About:

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