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