proposition: Lemma mkAnd_unfold: forall l1 l2, wf_re (CAnd l1) -> wf_re (CAnd l2) -> mkAnd (CAnd l1) (CAnd l2) = CAnd (undup (merge' (sort' l1) (sort' l2))).
proof: Proof. move => l1 l2; rewrite !wf_re_CAnd. case/and4P => hs1 hu1 hst1 ha1. case/and4P => hs2 hu2 hst2 ha2 /=. have : (2 <= size (undup (merge' (sort' l1) (sort' l2)))). rewrite (@perm_size _ (undup (merge' (sort' l1) (sort' l2))) (undup (l1++l2))). apply (@leq_trans (size l2)). done. rewrite -{1}(@undup_id _ l2). apply tool_undup_size. done. apply uniq_perm. by apply undup_uniq. by apply undup_uniq. move => u. by rewrite !mem_undup mem_merge !mem_cat !mem_sort. clear hu1 hu2 hst2 hst2 ha1 ha2. rewrite /mkAnd. case: (undup (merge' (sort' l1) (sort' l2))) => //. move => hd. by case => //=. 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)