proposition: Lemma well_formed_cf_subst_is_well_formed_cf_subst_aux : forall sigma, well_formed_cf_subst sigma -> (forall v, nb_occ X.eq_bool v sigma <= 1) -> exists sigma', well_formed_subst sigma' /\ is_subst_canonical_form sigma' sigma.
proof: Proof. unfold well_formed_cf_subst, is_subst_canonical_form; intros sigma Wsigma Nb_occ_sigma; induction sigma as [ | [v1 t1] sigma]. exists (nil : substitution); split; trivial; intro v; simpl; trivial. elim IHsigma. intros sigma' [Wsigma' Hsigma']; assert (Wt1 : well_formed_cf t1). generalize (Wsigma v1); simpl; generalize (X.eq_bool_ok v1 v1); case (X.eq_bool v1 v1); [ intros _ | intros v1_diff_v1]; trivial; absurd (v1=v1); trivial. elim (well_formed_cf_is_well_formed_cf _ Wt1); intros u1 [Wu1 Hu1]; exists ((v1,u1)::sigma'); split; intro v; simpl; case (X.eq_bool v v1); trivial. apply Wsigma'. subst; trivial. apply Hsigma'. intro v; generalize (Wsigma v) (Nb_occ_sigma v); simpl; case (X.eq_bool v v1); trivial. generalize (some_nb_occ_Sn X.eq_bool v sigma); case (find X.eq_bool v sigma). intros t H; generalize (H _ (eq_refl _)); clear H; intros H _ H'. destruct (nb_occ X.eq_bool v sigma) as [ | no]; [ absurd (1 <= 0) | absurd (S(S no) <= 1) ]; auto with arith. intros; exact I. intro v; generalize (Nb_occ_sigma v); simpl; case (X.eq_bool v v1); trivial; auto with arith. Qed.
imports: Coq(Relations List Arith Morphisms) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory_spec equational_theory)