proposition: Lemma sat_cons (M : cmodel) (w : M) C : (forall s, s \in C -> eval (interp s) w) -> ~~ gen_dec C.
proof: Proof. move => H. apply/negP => /gen_decP/gen_correctness. apply. by exists M; exists w. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.K(K_def demo gentzen)