proposition: Lemma canonical_regexp_eq_axiom : Equality.axiom (fun r1 r2 => compare r1 r2 == Eq).
proof: Proof. move => r1 r2. apply: (iffP idP). - move/eqP => h. by apply: compare_eq_axiom. - move => ->. by rewrite (compare_refl r2). 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)