proposition: Lemma ssubr_transV : forall y z, ssubr (Void char) y -> ssubr y z -> ssubr (Void char) z.
proof: Proof. elim => [ | | | u | c hc | c1 hc1 c2 hc2 | c1 hc1 c2 hc2 | c1 hc1 c2 hc2 | c hc ] z //. rewrite ssubrPlus2; case/andP => h1 h2. elim : z => [ | | | v | c' _ | c1' hc1' c2' hc2' | c1' _ c2' _ | c1' _ c2' _ | c _ ] //; try by( rewrite ssubrPlus1 //; case/orP => hu; [rewrite hc1 | rewrite hc2] ). rewrite !ssubrPlus2; case/andP => h3 h4. by rewrite hc1' // 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)