proposition: Lemma list_permut_flatten : forall f l1 l2, permut l1 l2 -> permut (flatten f l1) (flatten f l2).
proof: Proof. intros f l1; induction l1 as [ | t1 l1]; intros l2 P. rewrite (permut_nil (permut_sym P)); apply permut_refl. assert (In_t1 : mem (@eq _) t1 l2). rewrite <- P; left; reflexivity. destruct (mem_split_set _ _ eq_bool_ok _ _ In_t1) as [t1' [l2' [l2'' [t1_eq_t1' [H _]]]]]; simpl in t1_eq_t1'; simpl in H; subst l2; assert (P' : permut (flatten f l1) (flatten f (l2' ++ l2''))). apply IHl1. rewrite <- permut_cons_inside in P; trivial. dummy t1 t1' t1_eq_t1'; subst t1'. rewrite flatten_app; simpl; destruct t1 as [v1 | f1 ll1]. rewrite <- permut_cons_inside. rewrite <- flatten_app; trivial. reflexivity. generalize (F.Symb.eq_bool_ok f f1); case (F.Symb.eq_bool f f1); [intro f_eq_f1; subst f1 | intros _]. transitivity (ll1 ++ flatten f (l2' ++ l2'')). rewrite <- permut_app1; trivial. rewrite flatten_app; do 2 rewrite <- app_ass; rewrite <- permut_app2; apply list_permut_app_app. rewrite <- permut_cons_inside. rewrite <- flatten_app; trivial. reflexivity. Qed.
imports: Coq(Relations List Arith Morphisms) CoLoR(more_list list_permut list_sort term_spec term_o equational_theory_spec equational_theory)