proposition: Lemma ssubrPlus_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 (Plus a c) r -> forall x, x \in r -> x \in (Plus a c).
proof: Proof. move => a c ha hc r. elim : r => [ | | |s | d _ | c1 hc1 c2 hc2 | c1 hc1 c2 hc2 | c1 hc1 c2 hc2 | d _ ]; try (by rewrite ssubrPlus1 //; case/orP => hu x hx; rewrite !inE; apply/orP; [left; apply (ha _ hu) | right; apply (hc _ hu)] ). - by rewrite ssubrPlus1. rewrite ssubrPlus2; case/andP => h1 h2 x. rewrite -topredE /=. case/orP => hu. - by apply: hc1. by apply: hc2. 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)