Nuprl - Proof: eqof eq btrue

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: eqof eq btrue

A:Type, d:EqDecider(A), i:A. (eqof(d)(i,i)) ~ true

By:	Auto THEN Analyze -2 THEN InstHyp [i;i] -2 THEN Unfold `eqof` 0 THEN Reduce 0

Generated subgoal:

1 1. A : Type
2. eq : AA
3. x,y:A. x = y  eq(x,y)
4. i : A
5. i = i  eq(i,i)
  (eq(i,i)) ~ true
1 step

About:

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html