proposition: Lemma ssubrAnd_ok : forall a c, (forall b, ssubr a b -> forall x, x \in b -> x \in a) -> (forall d, ssubr c d -> forall x, x \in d -> x \in c) -> forall r, ssubr (And a c) r -> forall x, x \in r -> x \in (And a c).
proof: Proof. move => a c ha hc. elim => [ | | |t | d _ | d1 hd1 d2 hd2 | d1 _ d2 _ | d1 _ d2 _ | d _ ] //. - rewrite ssubrPlus2. case/andP => h1 h2 x. rewrite -topredE /=; case/orP => hu; [ by apply hd1 | by apply hd2]. rewrite ssubrAnd; case/andP => h1 h2 x. rewrite -!topredE /=. case/andP => h3 h4. apply/andP. by rewrite (ha d1 h1 x h3) (hc d2 h2 x h4). 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)