1. MsgA List
2. u : MsgA
3. v : MsgA List
4. (A,Bv.A ||+ B)  (Av.Feasible(A))  Feasible((v))
  (A,B[u / v].A ||+ B)  (A[u / v].Feasible(A))  Feasible(u  (v))

By:	Auto THEN RWO Thm* T:Type{i}, x:T, L:T List, P:(TTProp{i'}). Thm* (x,y[x / L].P(x,y))  (x,yL.P(x,y)) & (yL.P(x,y)) -2 THEN RWO Thm* P:(TProp), x:T, L:T List. (y[x / L].P(y))  P(x) & (yL.P(y)) -1 THEN Assert u ||+ (v)

1	5. (A,Bv.A ||+ B) 6. (Bv.u ||+ B) 7. Feasible(u) 8. (Av.Feasible(A))   u ||+ (v)	1 step
2	5. (A,Bv.A ||+ B) 6. (Bv.u ||+ B) 7. Feasible(u) 8. (Av.Feasible(A)) 9. u ||+ (v)   Feasible(u  (v))	1 step

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