proposition: Lemma flatten_cf : forall f t1 t2, arity f = AC -> well_formed_cf t1 -> well_formed_cf t2 -> permut (flatten f (t1 :: nil)) (flatten f (t2 :: nil)) -> t1 = t2.
proof: Proof. intros f t1 t2 Af Wt1 Wt2; destruct t1 as [v1 | f1 l1]; destruct t2 as [v2 | f2 l2]. simpl; intros; apply permut_length_1; trivial. simpl; generalize (F.Symb.eq_bool_ok f f2); case (F.Symb.eq_bool f f2); [intros f_eq_f2; subst f2 | intros f_diff_f2]. rewrite <- app_nil_end; intro P; absurd (2 <= 1); auto with arith. generalize (permut_length P); simpl; intro L; pattern 1 at 2; rewrite L; auto with arith; apply well_formed_cf_length with f; trivial. intro P; apply permut_length_1; trivial. simpl; generalize (F.Symb.eq_bool_ok f f1); case (F.Symb.eq_bool f f1); [intros f_eq_f1; subst f1 | intros f_diff_f1]. rewrite <- app_nil_end; intro P; absurd (2 <= 1); auto with arith. generalize (permut_length P); simpl; intro L; pattern 1 at 2; rewrite <- L; auto with arith; apply well_formed_cf_length with f; trivial. intro P; apply permut_length_1; trivial. simpl; generalize (F.Symb.eq_bool_ok f f1); case (F.Symb.eq_bool f f1); [intros f_eq_f1; subst f1 | intros f_diff_f1]; (generalize (F.Symb.eq_bool_ok f f2); case (F.Symb.eq_bool f f2); [intros f_eq_f2 P; subst f2 | intros f_diff_f2 P]). apply (f_equal (fun l => Term f l)); do 2 rewrite <- app_nil_end in P; apply sort_is_unique; trivial; apply well_formed_cf_sorted with f; trivial. absurd (2 <= 1); auto with arith. rewrite <- app_nil_end in P; generalize (permut_length P); simpl; intro L; pattern 1 at 2; rewrite <- L; auto with arith; apply well_formed_cf_length with f; trivial. absurd (2 <= 1); auto with arith. rewrite <- app_nil_end in P; generalize (permut_length P); simpl; intro L; pattern 1 at 2; rewrite L; auto with arith; apply well_formed_cf_length with f; trivial. apply permut_length_1; trivial. Qed.
imports: Coq(Relations List Arith Morphisms) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory_spec equational_theory)