1. A : Type
2. eq : EqDecider(A)
3. B : AType
4. P : x:AB(x)Prop
5. x : A
6. v : B(x)
7. y:A. (eqof(eq)(x,y)  false)  P(y,v)
  P(x,v)

By:	BackThru -1 THEN RWO Thm* d:EqDecider(A), i:A. (eqof(d)(i,i)) ~ true 0 THEN Reduce 0

None

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