proposition: Lemma wf_re_CPlus: forall l, wf_re (CPlus l) = [&& (size l >= 2) , uniq l , sorted cregexp_le l & all wf_re l].
proof: Proof. by move => l. 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)