proposition: Theorem perm_flatten_listReplace : forall b (A : Set)(ls1 : list (list A))(ls2 : list A) (a : A), Permutation (flatten ls1) ls2 -> Permutation (flatten (listReplace ls1 b (nth b ls1 nil ++ (a :: nil)) nil)) (a :: ls2).
proof: Proof. induction b; intuition; simpl in *. destruct ls1. simpl in *. apply Permutation_nil in H. subst. eapply Permutation_refl. simpl in *. rewrite <- app_cons_eq. eapply Permutation_trans. eapply Permutation_app_comm. rewrite <- app_comm_cons. econstructor. eapply Permutation_trans. eapply Permutation_app_comm. trivial. destruct ls1. simpl in *. eapply Permutation_nil in H. subst. eapply perm_flatten_listReplace_nil . simpl in *. eapply Permutation_trans. eapply Permutation_app. eapply Permutation_refl. eapply IHb. eapply Permutation_refl. eapply Permutation_trans. eapply Permutation_app_comm. rewrite <- app_comm_cons. econstructor. eapply Permutation_trans. eapply Permutation_app_comm. trivial. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation