1. A : Type
2. eq : EqDecider(A)
3. d : A List
4. d1 : A List
  (||d @ filter(a.deq-member(eq;a;d);d1)||=0) = ((||d||=0)(||d1||=0))

1	3. d1 : A List   (||filter(a.true;d1)||=0) = (||d1||=0)	2 steps
2	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))	1 step

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