proposition: Lemma CAnd_sort : forall le l, CAnd (sort le l) =i CAnd l.
proof: Proof. move => le l u. rewrite ! CAnd_all. apply/allP/allP. - move => h x hIn; apply h. by rewrite mem_sort. - move => h x hIn; apply h. by move: hIn; rewrite mem_sort. 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)