IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
symmetric rel or T:Type, R1,R2:(TTProp).
(Sym x,y:T. xR1y) (Sym x,y:T. xR2y) (Sym x,y:T. x (R1R2) y)
By:
Unfolds [`sym`;`rel_or`] 0 THEN Reduce 0 THEN ParallelOp -1 THEN EasyHyp
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
T:Type, R1,R2:(T
T
(Sym x,y:T. x R1 y) 
(Sym x,y:T. x R2 y) 
R2) y)
