proposition: Lemma mkPlus_unfold3: forall l1 r2, wf_re (CPlus l1) -> wf_re r2 -> (r2 != CVoid /\ (forall l, r2 != CPlus l) ) -> mkPlus r2 (CPlus l1) = CPlus (undup (merge' [::r2] (sort' l1) )).
proof: Proof. move => l1 r2 h1 h2 h3. rewrite mkPlusC. rewrite /merge' merge_sort_sym =>//. by apply: mkPlus_unfold2. by apply: leS_trans. by apply: leS_antisym. by apply: leS_total. apply: sort_sorted. by apply: leS_total. 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)