T:Type, P:(TProp), A,B:T List.
  A = B  (i:||A||. P(A[i]))  A = B  {x:T| P(x) } List

By:	Auto THEN AssertBY (||B|| = ||A||) (HypSubst -2 0) THEN AssertBY (i:||B||. P(B[i])) (RevHypSubst -3 0)

1

1. T : Type 2. P : TProp 3. A : T List 4. B : T List 5. A = B 6. i:||A||. P(A[i]) 7. ||B|| = ||A||   8. i:||B||. P(B[i])   A = B  {x:T| P(x) } List

4 steps

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