proposition: Lemma flatten_cf_cf : forall f t1 t2, arity f = AC -> well_formed t1 -> well_formed t2 -> permut (flatten f (canonical_form t1 :: nil)) (flatten f (canonical_form t2 :: nil)) -> canonical_form t1 = canonical_form t2.
proof: Proof. intros f t1 t2 Af Wt1 Wt2 P; apply flatten_cf with f; trivial. apply well_formed_cf_is_well_formed_cf_conv; exists t1; split; trivial. apply well_formed_cf_is_well_formed_cf_conv; exists t2; split; trivial. Qed.
imports: Coq(Relations List Arith Morphisms) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory_spec equational_theory)