proposition: Lemma flat_map_ext : forall (A B : Type)(f g : A -> list B), (forall a, f a = g a) -> forall l, flat_map f l = flat_map g l.
proof: Proof. intros A B f g Hext l. rewrite 2 flat_map_concat_map. now rewrite (map_ext _ g). Qed.
imports: PeanoNat