Nuprl - Proof: append is nil 2 1

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

T:Type, x:T, l:T List. [x / l] = nil

False
2. T : Type
3. T List
4. u : T
5. v : T List
6.

l2:T List. (v @ l2) = nil

v = nil & l2 = nil

l2:T List. [u / (v @ l2)] = nil

[u / v] = nil & l2 = nil

By:	Analyze 0 THEN ListInd -1 THEN Try (FwdThru 1 [-1] ORELSE FwdThru 1 [-2])

Generated subgoals:

None

About:

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