T:Type, ll1,ll2:(T List) List. ll1  ll2  concat(ll1)  concat(ll2)

1

1. T : Type 2. ll1 : (T List) List 3. ll2 : (T List) List 4. l : (T List) List 5. ll2 = (ll1 @ l)   l@0:T List. concat(ll1 @ l) = (concat(ll1) @ l@0)

1 step

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