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