proposition: Lemma has_eps_canE : forall r, has_eps_can r = ([::] \in r) .
proof: Proof. apply creg_ind with (fun l => hec_forall l = (all (fun xx => [::] \in xx) l)/\ hec_exists l = (has (fun xx => [::] \in xx) l)). + done. + done. + done. + by move => s. + by move => c. + move => l [ _ hl ] /= ; move : hl. rewrite /hec_exists ; move => ->. rewrite -topredE /= /mem_creg /=. by elim: l => [ | hd tl hi] //=; rewrite hi. + move => l [ hl _ ] /= ; move : hl. rewrite /hec_forall ; move => ->. rewrite -topredE /= /mem_creg /=. by elim: l => [ | hd tl hi] //=; rewrite hi. + move => l [ hl _ ] /= ; move : hl. rewrite /hec_forall ; move => ->. rewrite -topredE /= /mem_creg /=. elim: l => [ | hd tl hi] //=. apply/andP/concP. * case => hhd hall. exists [::] => //. exists [::]; split => //=; split => //=. by rewrite -topredE /= /mem_creg /= -hi. * case => [v1 [v2 [hv [hv1 hv2]]]]. move: hv. case: v1 hv1 => //= hv1 heq. by rewrite hv1 hi heq. + by move => c h /= ; rewrite h. + by []. + move => c hc l [hl1 hl2] /=; split. - by congr andb. - by congr orb. 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)