proposition: Lemma regular_quotL_aux : regular quotL.
proof: Proof. Proof using acc_L2 dec_L1. pose S := [seq q | q <- enum A & dec_L1 q]. pose L (q:A) := mem (dfa_lang (A_start q)). pose R x := exists2 a, a \in S & L a x. suff: quotL =p R. { apply: regular_ext. apply: regular_bigU => q qS. by exists (A_start q). } move => y; split. - case => x H1 /acc_L2 H2. exists (delta_s A x). + apply/mapP. exists (delta_s A x) => //. rewrite mem_filter mem_enum inE andbT. apply/dec_eq. by exists x. + by rewrite /L topredE -A_start_cat. - case => ? /mapP [q]. rewrite mem_filter mem_enum inE andbT => /dec_eq [x L1_x <- ->]. rewrite /L topredE -A_start_cat => Hxy. exists x => //. exact/acc_L2. Qed.
imports: mathcomp(all_ssreflect) RegLang(misc languages)