Nuprl - Proof: rel star of equiv 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: rel star of equiv 1 1 1

1. T : Type
2. E : T

Prop
3. EquivRel(T)(_1 E _2)
4. x : T
5. y : T
6. x = y

x E y

By:	HypSubst -1 0 THEN UseEquiv

Generated subgoals:

None

About:

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