T:Type, L:T List. L  {x:T| (x  L) } List

1	1. T : Type 2. T List 3. u : T 4. v : T List 5. v  {x:T| (x  v) } List   u  {x:T| (x  [u / v]) }	2 steps
2	1. T : Type 2. T List 3. u : T 4. v : T List 5. v  {x:T| (x  v) } List   v  {x:T| (x  [u / v]) } List	3 steps

About: IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html