Nuprl - Proof: symmetrized preorder 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: symmetrized preorder 1

1. T : Type
2. R : T

Prop
3. Refl(T;x,y.R(x,y))
4. Trans x,y:T. R(x,y)

Refl(T;a,b.R(a,b) & R(b,a))

By:	TryOnAllClauses (Unfold `refl`) THEN HypBackchain

Generated subgoals:

None

About:

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