proposition: Lemma flattenP (T : eqType) (ss : (seq (seq T))) a : reflect (exists2 s, s \in ss & a \in s) (a \in flatten ss).
proof: Proof. elim: ss => //= [|s0 ss IHss]. rewrite in_nil. constructor => [[s]]. by rewrite in_nil. rewrite mem_cat. apply: (iffP orP) => [[H|/IHss [s in_ss in_s]]|[s]]. - exists s0; by rewrite ?mem_head. - exists s => //. by rewrite in_cons in_ss. - rewrite in_cons. case/orP => [/eqP->|*]; auto. right. apply/IHss. by eexists. Qed.
imports: mathcomp(all_ssreflect) Relations CompDecModal.libs(edone bcase)