Nuprl - Proof: append nil sq 1

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

1. T : Type
2. T List
3. u : T
4. v : T List
5. (v @ nil) ~ v

[u / (v @ nil)] ~ [u / v]

By:	Subst ((v @ nil) ~ v) 0 THEN Trivial

Generated subgoals:

None

About:

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