IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
deq property T:Type, d:EqDecider(T), x,y:T. x = y eqof(d)(x,y)
By:
Unfolds [`deq`;`eqof`] 0 THEN Analyze 2 THEN All Reduce THEN BackThru 3
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
T:Type, d:EqDecider(T), x,y:T. x = y 
eqof(d)(x,y)
