proposition: Lemma mkAnd_id : forall r, wf_re r -> mkAnd r r = r.
proof: Proof. case => [ | | | s | c | l | l | l | c ] //=; try ( by rewrite /mkAnd compare_refl). - move => h. rewrite mkAnd_unfold => //. f_equal. apply : (@sorted_eq _ cregexp_le). by apply: leS_trans. by apply: leS_antisym. apply: undup_sorted. by apply: leS_trans. apply: merge_sorted. by apply: leS_total. apply : sort_sorted. by apply : leS_total. apply: sort_sorted. by apply: leS_total. by case/and4P: h. apply: uniq_perm. apply undup_uniq. by case/and4P: h. move => u. rewrite mem_undup mem_merge mem_cat !mem_sort. by apply/orP/idP; [case | left]. - case: c => [ | | | s | c' | l | l | l | c' ] //= ; by rewrite toolmkAnd3 // compare_refl. 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)