proposition: Lemma in_flatten_iff : forall {A} x seqs, @List.In A x (flatten seqs) <-> exists seq, List.In x seq /\ List.In seq seqs.
proof: Proof. intros; unfold flatten. induction seqs; simpl. firstorder. rewrite in_app_iff. rewrite IHseqs. split. intros [ in_head | [seq (in_seqs & in_seq) ] ]; eauto. intros [ seq ( in_seq & [ eq_head | in_seqs ] ) ]; subst; eauto. Qed.
imports: Coq.Lists.List Coq.Lists.SetoidList Fiat.Common Coq.Arith.Arith