proposition: Lemma well_formed_cf_subst_is_well_formed_cf_subst : forall sigma, well_formed_cf_subst sigma -> exists sigma', well_formed_subst sigma' /\ is_subst_canonical_form sigma' sigma.
proof: Proof. assert (E : equivalence _ (@eq variable)). repeat split. intros t1 t2 t3 H1 H2; subst; reflexivity. intros t1 t2 H; subst; reflexivity. intros sigma Wsigma; elim (reduce_assoc_list _ X.eq_bool_ok E sigma); intros sigma1 [Nb_occ H]; elim (well_formed_cf_subst_is_well_formed_cf_subst_aux (sigma := sigma1)); trivial. intros sigma' [Wsigma' H']; exists sigma'; split; trivial; intro v; rewrite H; apply H'. intro v; rewrite <- H; apply Wsigma. Qed.
imports: Coq(Relations List Arith Morphisms) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory_spec equational_theory)