T:Type, P:(TProp), R1,R2:(TTProp).
  R1 preserves P  R2 preserves P  R1  R2 preserves P

By:	Unfolds [`rel_or`;`preserved_by`] 0 THEN Reduce 0 THEN Analyze -1 THEN AllHyps (h.InstHyp [x;y] h THEN Complete Auto)

None

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