proposition: Lemma CAnd_mem_match : forall l1 l2 u, (u \in (match undup (merge' (sort' l1) (sort' l2)) with | [::] => CNot CVoid | [:: r] => r | rs => CAnd rs end)) = (u \in CAnd (l1 ++ l2)).
proof: Proof. rewrite /merge'. move => l1 l2. have : (undup (merge cregexp_le (sort' l1) (sort' l2)) =i (l1++l2)). by move => u; rewrite mem_undup mem_merge !mem_cat !mem_sort. case: (undup (merge cregexp_le (sort' l1) (sort' l2))) => //. - move => h u. rewrite CAnd_all. by rewrite -(eq_all_r h) in_CAll. - move => hd0. case => //. move => h u. by rewrite CAnd_all -(eq_all_r h) all_seq1. move => hd tl h u. rewrite !CAnd_all. by rewrite -(eq_all_r h). 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)