proposition: Lemma is_subst_cf_is_subst_cf : forall sigma, is_subst_canonical_form sigma (map_subst (fun _ t => canonical_form t) sigma).
proof: Proof. intros sigma; unfold is_subst_canonical_form. intro v; rewrite subst_comp_is_subst_comp_aux1. destruct (find X.eq_bool v sigma); trivial. Qed.
imports: Coq(Relations List Arith Morphisms) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory_spec equational_theory)