1. A : Type
2. eq : EqDecider(A)
3. A List
4. u : A
5. v : A List
6. x:A. deq-member(eq;x;v)  (x  v)
  x:A. (eqof(eq)(u,x)  deq-member(eq;x;v))  (x  [u / v])

By:	((ParallelOp -1 THEN RW assert_pushdownC 0) (THEN ((RWO Thm* l:T List, a,x:T. (x  [a / l])  x = a  (x  l) 0) (THEN ((RWO "deq_property<" 0)) THEN ParallelOp -1 THEN ThinTrivial THEN Trivial

None

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