proposition: Lemma total_ordering_eq_subst : forall c sigma tau, (forall v, find X.eq_bool v sigma = find X.eq_bool v tau) -> is_a_total_oc_ordering sigma c = is_a_total_oc_ordering tau c.
proof: Proof. intro c; induction c as [ | v c]; intros sigma tau H; simpl. trivial. rewrite H; rewrite (IHc sigma tau); trivial. Qed.
imports: Coq(Arith Wf_nat Wellfounded List Multiset Relations) CoLoR(closure decidable_set ordered_set more_list list_permut list_set list_sort dickson term_spec term)