proposition: Lemma bregexp_eqP : forall (r1 r2:bregexp), reflect (r1 ≡ r2) (bregexp_eq r1 r2).
proof: Proof. move => r1 r2. have h1 : (r1,r2,[::]) \in build_list_fun r1 r2. rewrite /build_list_fun. apply: (linclP [:: (r1,r2,[::])]); first by apply: l1. by rewrite /= in_cons eq_refl. have h2: r_subset sim3 (DER (build_list_fun r1 r2)) (build_list_fun r1 r2). rewrite /build_list_fun; apply: l3. by rewrite lminus_incl. apply: (iffP allP). - rewrite /bregexp_eq => h. apply EQUIV3. move => e f. rewrite /set_pair_der => [[s he hf]]. rewrite (has_eps_sim he) (has_eps_sim hf) !has_epsE. case: (tool_bl h2 h1 s) => e' [f' [v' [h'1 h'2 h'3]]]. rewrite (h'2 [::]) (h'3 [::]) -!has_epsE. move: (h (e',f',v') h'1). rewrite /delta2 => heq. by rewrite (eqP heq). - move => h [[e f] v] hIn. rewrite /delta2 !has_epsE. have: (Prod (set_pair_ders r1 r2) bT (e,f,v)). by apply: (gpred_listP2 hIn); apply: l2. case => [[s -> ->]] _. apply/eqP. by apply in_wder_compat. Qed.
imports: Coq(RelationClasses) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue gfinset regexp finite_der)