proposition: Lemma toolmkPlus2_l: forall r, (r != CVoid /\ (forall l, r != CPlus l)) -> forall l, mkPlus r (CPlus l) = match undup (merge' [::r] (sort' l)) with | [::] => CVoid | [:: c] => c | s => CPlus s end.
proof: Proof. case => [ | | | s | c | l | l | l | c ] [] //= _. move => h. move/negP: (h l). 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)