proposition: Lemma ssublConc : forall r1 r2 s1 s2, ssubl (Conc r1 r2) (Conc s1 s2) = ssubl r1 s1 && ssubl 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)