proposition: Lemma toolmkPlus : forall c, [\/ c == CVoid , (exists l , c == CPlus l) | (c != CVoid /\ (forall l, c != CPlus l)) ].
proof: Proof. case => [ | | | s | c | l | l | l | c ] //=; try ( by apply Or33;split). - by apply : Or31. - by apply : Or32; exists 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)