proposition: Lemma mkAnd_unfold3: forall l1 r2, wf_re (CAnd l1) -> wf_re r2 -> [/\ r2 != CVoid , r2 != CNot CVoid & (forall l, r2 != CAnd l)] -> mkAnd r2 (CAnd l1) = CAnd (undup (merge' [::r2] (sort' l1) )).
proof: Proof. move => l1 r2 h1 h2 h3. rewrite mkAndC. rewrite /merge' merge_sort_sym =>//. by apply: mkAnd_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)