Nuprl - Proof: rel star weakening

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

T:Type, x,y:T, R:(T

Prop). x = y

(x (R^*) y)

By:	Auto THEN Unfold `rel_star` 0 THEN Reduce 0 THEN InstConcl [0] THEN ReduceExp 0

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