T:Type, l1,l2,l3:T List. l1  l2  l2  l3  l1  l3

1

1. T : Type 2. l1 : T List 3. l2 : T List 4. l3 : T List 5. l4 : T List 6. l2 = (l1 @ l4) 7. l : T List 8. l3 = (l2 @ l)   l3 = (l1 @ l4 @ l)

2 steps

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