proposition: Theorem well_formed_cf_apply_subst : forall sigma, well_formed_cf_subst sigma -> forall t, well_formed_cf t -> well_formed_cf (apply_cf_subst sigma t).
proof: Proof. intros sigma Wsigma t Wt; elim (well_formed_cf_is_well_formed_cf _ Wt); intros u [Wu Hu]; subst; elim (well_formed_cf_subst_is_well_formed_cf_subst Wsigma); intros tau [Wtau Htau]; rewrite apply_cf_subst_is_sound with tau sigma u; trivial; apply well_formed_cf_is_well_formed_cf_conv; exists (apply_subst tau u); split; trivial; apply well_formed_apply_subst; trivial. Qed.
imports: Coq(Relations List Arith Morphisms) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory_spec equational_theory)