proposition: Lemma bregexp_subP : forall r1 r2, reflect (SUB r1 r2) (bregexp_sub r1 r2).
proof: Proof. rewrite /SUB /bregexp_sub => r1 r2. apply: (iffP idP). - move/bregexp_eqP => h. by apply SUB2. - move => h. apply/bregexp_eqP. by apply SUB2. Qed.
imports: Coq(RelationClasses) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue gfinset regexp finite_der)