fact: Record Rewrite_ordering : Type := mkRewrite_ordering { rew_ord_rel :> relation term; rew_ord_subs : substitution_closed rew_ord_rel; rew_ord_cont : context_closed rew_ord_rel }.
imports: CoLoR(SN ASubstitution ATerm RelUtil AContext LogicUtil VecUtil NaryFunction) Coq(List)