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. case/andP => /andP [/negbTE -> /allP H] _. split => // x. case inC: (fV x^+ \in C) => //=. apply: negbTE. apply: H _ inC. Qed.
imports: Relations Classical_Pred_Type mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base) CompDecModal.PDL(PDL_def)