proposition: Lemma wf_re_can : forall c, wf_re (canonize c).
proof: Proof. elim => [ | | | s | c | c1 hc1 c2 hc2 | c1 hc1 c2 hc2 | c1 hc1 c2 hc2 | c ] //=. - by apply wf_CStar. - by apply wf_CPlus. - by apply wf_CAnd. - by apply wf_CConc. - by apply wf_CNot. 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)