proposition: Lemma flattenP (A : seq (seq T)) x : reflect (exists2 s, s \in A & x \in s) (x \in flatten A).
proof: Proof. elim: A => /= [|s A IH_A]; [by right; case | rewrite mem_cat]. by apply: equivP (iff_sym exists_cons); apply: (orPP idP IH_A). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)