proposition: Lemma mkAndA : forall r1 r2 r3, wf_re r1 -> wf_re r2 -> wf_re r3 -> mkAnd (mkAnd r1 r2) r3 = mkAnd r1 (mkAnd r2 r3).
proof: Proof. move => r1 r2 r3 h1 h2 h3. rewrite mkAndAC => //. rewrite (mkAndC r1 r3). rewrite -mkAndAC => //. by rewrite (mkAndC r3 r2) mkAndC. 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)