T:Type, l:T List, a,x,y:T.
  x before y  [a / l]  x = a & (y  l)  x before y  l

By:	(Unfold `l_before` 0 THEN RWO Thm* x:T, L:T List. (x  L)  [x]  L 0) THEN (RWO (Thm* x1,x2:T, L1,L2:T List. (Thm* [x1 / L1]  [x2 / L2]  x1 = x2 & L1  L2  [x1 / L1]  L2 (0)

None

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