proposition: Lemma ssubrAtom_ok : forall s b, ssubr (Atom s) b -> forall x, (x \in b) -> (x \in (Atom s) ).
proof: Proof. move => s; elim => //. - by move => t; rewrite {1}/ssubr => h; rewrite (eqP h). move => r1 hr1 r2 hr2. rewrite ssubrPlus2. case/andP => h1 h2 x. rewrite -!topredE /=; case/orP => hu. - move: (hr1 h1 x hu). by rewrite -topredE /=. move: (hr2 h2 x hu). by rewrite -topredE /=. 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)