Nuprl - Proof: member append 1

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

1. T : Type
2. x : T
3. T List

l2:T List. (x

l2)

nil)

l2)

By:

Auto

Generated subgoals:

1 4. l2 : T List
5. (x  l2)
  (x  nil)  (x  l2)
1 step

2 4. l2 : T List
5. (x  nil)  (x  l2)
  (x  l2)
2 steps

About:

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

1	4. l2 : T List 5. (x l2) (x nil) (x l2)	1 step
2	4. l2 : T List 5. (x nil) (x l2) (x l2)	2 steps