proposition: Lemma ssubrStar_ok : forall a, (forall b, ssubr a b -> forall x, x \in b -> x \in a) -> forall b, ssubr (Star a) b -> forall x, x \in b -> x \in (Star a).
proof: Proof. move => a ha. elim => [ | | |t | d _ | d1 hd1 d2 hd2 | d1 _ d2 _ | d1 _ d2 _ | d _ ] //. - rewrite ssubrStar => 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 ssubrPlus2; case/andP => h1 h2 x; rewrite -topredE /=; case/orP => hx ; [rewrite (hd1 h1 x hx) | rewrite (hd2 h2 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)