proposition: Lemma starI l vv : (forall v, v \in vv -> v \in l) -> flatten vv \in star l.
proof: Proof. elim: vv => /= [//| v vv IHvv /forall_cons [H1 H2]]. exact: star_cat _ (IHvv _). Qed.
imports: HB(structures) mathcomp(all_ssreflect) RegLang(misc)