definition reverse_pordered_set: pordered_set → pordered_set.
intros (p); apply (mk_pordered_set (reverse_excedence p));
generalize in match (reverse_excedence p); intros (E); cases E (T f cRf cTf);
definition reverse_pordered_set: pordered_set → pordered_set.
intros (p); apply (mk_pordered_set (reverse_excedence p));
generalize in match (reverse_excedence p); intros (E); cases E (T f cRf cTf);