proposition: Lemma toolmkAnd : forall c, [ \/ c == CVoid , c == CNot CVoid, (exists l , c == CAnd l) | [ /\ c != CVoid , c != CNot CVoid & (forall l, c != CAnd l)]].
proof: Proof. case => [ | | | s | c | l | l | l | c ]; try (by apply Or44). - by apply Or41. - apply Or43; by exists l. - case : c => [ | | | s | c' | l | l | l | c' ]; try (by apply Or44). by apply Or42. 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)