proposition: Lemma mkAndAC_and_and_and: forall l1 l2 l3, wf_re (CAnd l1) -> wf_re (CAnd l2) -> wf_re (CAnd l3) -> mkAnd (mkAnd (CAnd l1) (CAnd l2)) (CAnd l3) = mkAnd (mkAnd (CAnd l1) (CAnd l3)) (CAnd l2).
proof: Proof. move => l1 l2 l3 hw1 hw2 hw3. 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. 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. apply uniq_perm. by apply undup_uniq. by apply undup_uniq. move => u. rewrite !mem_undup !mem_merge !mem_cat !mem_sort !mem_undup !mem_merge !mem_cat !mem_sort. by rewrite orbAC. rewrite -mkAnd_unfold => //. by apply wf_CAnd. rewrite -mkAnd_unfold => //. by apply wf_CAnd. 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)