proposition: Lemma mem_mkNot : forall r, mkNot r =i CNot r.
proof: Proof. move => r. rewrite /eq_mem. symmetry. move : x. elim: r => //= . - move => c h u. rewrite -!topredE /= /mem_creg /=. by rewrite [compl _ u] negbK. 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)