proposition: Lemma mkStar_mem : forall r, CStar r =i mkStar r.
proof: Proof. move => r. elim: r => //=. - move => u. rewrite -topredE /= /mem_creg /=. rewrite !inE. apply/starP/idP. move => [[ | hd tl]] /=. move => _ ->. done. rewrite andbF //=. * move => heq. rewrite (eqP heq). exists [::]. done. done. - move => u. rewrite -topredE /= /mem_creg /=. rewrite !inE. apply/starP/idP. * move => [v]. elim: v => [ | hd tl hi] /=. by move => _ ->. move/andP => []. move/andP =>[]. move/negP. done. move => heq. rewrite (eqP heq). by exists [::]. move => c h. move => u. rewrite -!topredE /= /mem_creg /=. rewrite -[star _ _]/(_ \in star _). by rewrite star_id. 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)