proposition: Lemma DER_cat : forall l1 l2, sim_incl sim_dec3 (DER (l1 ++ l2)) ((DER l1) ++ (DER l2)).
proof: Proof. move => l1 l2; elim : l1 => [ | hd tl ] //=. - by apply : sim_incl_refl. - case: hd => [[hdl hdr] s] hi. rewrite !cat_cons. change [:: (der1 hdl, der1 hdr,true::s ), (der0 hdl, der0 hdr,false::s) & DER (tl ++l2)] with ([:: (der1 hdl, der1 hdr,true::s); (der0 hdl, der0 hdr,false::s)]++(DER (tl ++l2))). change [:: (der1 hdl, der1 hdr,true::s), (der0 hdl, der0 hdr,false::s) & DER tl ++ DER l2] with ([:: (der1 hdl, der1 hdr,true::s); (der0 hdl, der0 hdr,false::s)]++(DER tl ++ DER l2)). by rewrite sim_incl_lcongr. Qed.
imports: Coq(RelationClasses) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue gfinset regexp finite_der)