proposition: Lemma ssublConc_ok : forall a c, (forall b, ssubl a b -> forall x, x \in a -> x \in b) -> (forall d, ssubl c d -> forall x, x \in c -> x \in d) -> forall r, ssubl (Conc a c) r -> forall x, x \in (Conc a c) -> x \in r.
proof: Proof. move => a c ha hc. elim => [ | | |t | d _ | d1 hd1 d2 hd2 | d1 _ d2 _ | d1 _ d2 _ | d _ ] //. - by rewrite ssublPlus1 => //; case/orP => hu x hx; rewrite -topredE /=; apply/orP; [left; rewrite (hd1 hu x hx) | right; rewrite (hd2 hu x hx)]. rewrite ssublConc; case/andP => h1 h2 x. rewrite -!topredE /=. case/concP => u [v [hv [hu huv]]]. apply/concP; exists u. exists v; split => //; split; first by rewrite (ha d1 h1 u hu). by rewrite (hc d2 h2 v huv). 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)