proposition: Lemma flatten_app : forall f l1 l2, flatten f (l1 ++ l2) = (flatten f l1) ++ (flatten f l2).
proof: Proof. intros f l1; induction l1 as [ | [v1 | g1 ll1]]; simpl; trivial. intros l2; rewrite IHl1; trivial. intros l2; rewrite IHl1; generalize (F.Symb.eq_bool_ok f g1); case (F.Symb.eq_bool f g1); [intro f_eq_g1 | intro f_diff_g1]. rewrite app_ass; trivial. simpl; trivial. Qed.
imports: Coq(Relations List Arith Morphisms) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory_spec equational_theory)