proposition: Lemma ssublStar_ok : forall a, (forall b, ssubl a b -> forall x, x \in a -> x \in b) -> forall b, ssubl (Star a) b -> forall x, x \in (Star a) -> x \in b.
proof: Proof. move => a ha. elim => [ | | |t | d _ | d1 hd1 d2 hd2 | d1 _ d2 _ | d1 _ d2 _ | d _ ] //. - rewrite ssublStar => h x. rewrite -!topredE /=. case/starP => v. move/allP => h1 /= h2. apply/starP; exists v => //. apply/allP => y hy. case/andP: (h1 y hy) => hy1 hy2. apply/andP; split => //. by rewrite ?inE (ha d h y). by rewrite ssublPlus1 => //; case/orP => hu x hx; rewrite -topredE /=; apply/orP; [left; rewrite (hd1 hu x hx) | right; rewrite (hd2 hu x hx)]. Qed.
imports: Coq(RelationClasses Setoid Morphisms Permutation) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(regexp finite_der equiv)