proposition: Lemma has_epsE : forall e, has_eps e = ([::] \in e).
proof: Proof. elim => //= [c1 hc1 c2 hc2 | c1 hc1 c2 hc2 | c1 hc1 c2 hc2 | c1 hc1 ]. - by rewrite hc1 hc2. - by rewrite hc1 hc2. - rewrite hc1 hc2 => //. rewrite -[xx in _ = xx] topredE /=. by apply/idP/existsP; [exists ord0| case]. - by rewrite hc1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(bigop path) RegLang(languages) RegexpBrzozowski(glue)