proposition: Lemma concat_map_nil : forall A (l : list A), concat (List.map (fun x => x :: nil) l) = l.
proof: Proof. induction l. - reflexivity. - simpl. rewrite IHl. reflexivity. Qed.
imports: Coq(ssreflect List) Mon(SPropBase SPropMonadicStructures Monoid)