IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
fpf-all-single-decl113 1. A : Type
2. eq : EqDecider(A)
3. B : AType
4. P : x:AB(x)Prop
5. x : A 6. v : B(x)
7. P(x,v)
8. y : A 9. eqof(eq)(x,y) false P(y,v)
By:
RW assert_pushdownC -1 THEN Analyze -1 THEN RWO "deq_property<" -1
Type
false
P(y,v)
