proposition: Lemma mkPlusA : forall r1 r2 r3, wf_re r1 -> wf_re r2 -> wf_re r3 -> mkPlus (mkPlus r1 r2) r3 = mkPlus r1 (mkPlus r2 r3).
proof: Proof. move => r1 r2 r3 h1 h2 h3. rewrite mkPlusAC => //. rewrite (mkPlusC r1 r3). rewrite -mkPlusAC => //. by rewrite (mkPlusC r3 r2) mkPlusC. Qed.
imports: Coq(RelationClasses Setoid Morphisms) HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue regexp finite_der equiv)