proposition: Theorem perm_flatten_listReplace_nil : forall b (A : Set)(a : A), Permutation (flatten (listReplace nil b (a :: nil) nil)) (a :: nil).
proof: Proof. induction b; intuition; simpl in *. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation