proposition: Lemma mkPlus_unfold2: forall l1 r2, wf_re (CPlus l1) -> wf_re r2 -> (r2 != CVoid /\ (forall l, r2 != CPlus l)) -> mkPlus (CPlus l1) r2 = CPlus (undup (merge' (sort' l1) [::r2])).
proof: Proof. move => l1 r2; rewrite !wf_re_CPlus. case/and4P => hs1 hu1 hst1 ha1. move => hw2 hh. have : (2 <= size (undup (merge' (sort' l1) [::r2]))). rewrite (@perm_size _ (undup (merge' (sort' l1) [::r2])) (undup (l1++[::r2]))). apply (@leq_trans (size l1)). done. rewrite -{1}(@undup_id _ l1). apply tool_undup_size2. done. apply uniq_perm. by apply undup_uniq. by apply undup_uniq. move => u. by rewrite !mem_undup mem_merge !mem_cat !mem_sort. rewrite toolmkPlus2_r => //. clear hu1 hs1 hst1 ha1. case: (undup (merge' (sort' l1) [::r2])) => //. 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)