proposition: Lemma regular_expression_eq_axiom : Equality.axiom regexp_struct_eq.
proof: Proof. move => r1 r2. apply: (iffP idP); [ | by move => ->; apply regexp_struct_eq_refl]. elim :r1 r2 => [ | | | s | c hc | c1 hc1 c2 hc2 | c1 hc1 c2 hc2 | c1 hc1 c2 hc2 | c hc] //=. - by case. - by case. - by case. - case => //=. by move => t heq; rewrite (eqP heq). - case => //=. move => r hi; by rewrite (hc r hi). - case => //=. move => r1 r2. case/andP => hi1 hi2. by rewrite (hc1 r1 hi1) (hc2 r2 hi2). - case => //=. move => r1 r2. case/andP => hi1 hi2. by rewrite (hc1 r1 hi1) (hc2 r2 hi2). - case => //=. move => r1 r2. case/andP => hi1 hi2. by rewrite (hc1 r1 hi1) (hc2 r2 hi2). - case => //=. move => r hi; by rewrite (hc r hi). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue)