proposition: Lemma ssubrConc : forall r1 r2 s1 s2, ssubr (Conc r1 r2) (Conc s1 s2) = ssubr r1 s1 && ssubr r2 s2.
proof: Proof. by move => r1 r2 s1 s2 /=. 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)