proposition: Lemma LCF C : lcons C -> ((fF^+ \in C) = false) * (forall p, (fV p^+ \in C) && (fV p^- \in C) = false).
proof: Proof. move => /andP [/negbTE-> /allP H]. split => // p. case e: (_^+ \in _) => //=. by rewrite (negbTE (H _ e)). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.K(K_def)