[ apply (orelation_of_relation S T);
| intros; apply (orelation_of_relation_preserves_equality S T a a' e); ]
| apply orelation_of_relation_preserves_identity;
[ apply (orelation_of_relation S T);
| intros; apply (orelation_of_relation_preserves_equality S T a a' e); ]
| apply orelation_of_relation_preserves_identity;