-generalize in match (reverse_excedence p); intros (E); cases E (T f cRf cTf);
-simplify; apply mk_is_porder_relation; unfold; intros;
-[apply le_reflexive|apply (le_transitive ???? H H1);|apply (le_antisymmetric ??? H H1)]
+generalize in match (reverse_excedence p); intros (E);
+apply mk_is_porder_relation;
+[apply le_reflexive|apply le_transitive|apply le_antisymmetric]