proposition: Lemma CPlus_mem_match : forall l1 l2 u, (u \in (match undup (merge' (sort' l1) (sort' l2)) with | [::] => CVoid | [:: r] => r | rs => CPlus rs end)) = (u \in CPlus (l1 ++ l2)).
proof: Proof. rewrite /merge' /sort'. move => l1 l2. have : (undup (merge' (sort' l1) (sort' l2)) =i (l1++l2)). by move => u; rewrite mem_undup mem_merge !mem_cat !mem_sort. case: (undup (merge' (sort' l1) (sort' l2))) => //. - move => h u. rewrite CPlus_has. by rewrite -(eq_has_r h). - move => hd0. case => //. move => h u. by rewrite CPlus_has -(eq_has_r h) has_seq1. move => hd tl h u. rewrite !CPlus_has. by rewrite -(eq_has_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)