1. A : Type
2. eq : EqDecider(A)
3. u : A
4. v : A List
5. d1 : A List
  (||v @ filter(a.(eqof(eq)(u,a)  deq-member(eq;a;v));d1)||+1=0)
  =
  ((||v||+1=0)(||d1||=0))

By:	RWO Thm* as,bs:T List. ||as @ bs|| = ||as||+||bs||   0 THEN AutoBoolCase (||v||+1=0) THEN AutoBoolCase (||v||+||filter(a.(eqof(eq)(u,a)  deq-member(eq;a;v));d1)||+1=0)

None

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