1. A : Type
2. eq : EqDecider(A)
3. B : AType
4. x : A
5. y : A
6. v : B(x)
7. u : B(y)
8. x = y  v = u
  x : v || y : u

By:	Repeat (Unfolds [`fpf-ap`;`fpf-compatible`;`fpf-dom`;`fpf-single`] 0 THEN Reduce 0) THEN AllHyps (h.RW assert_pushdownC h THEN ElimOrFalse h THEN RWO "deq_property<" h)

1

9. x@0 : A 10. x = x@0 11. y = x@0   v = u  B(x@0)

1 step

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