proposition: Lemma gen_plain_sound C : gen (C, aVoid) -> ~ (exists M : cmodel, sat M C).
proof: Proof. move => /gen_def.soundness H. suff : ~ (exists M : fmodel, sat M C). { move => nF [M] [w] /Kstar_def.satA wC. apply: nF. case: (@small_models [af C]); first by do 2 eexists. move => {M w wC} => M _ [w] wC. exists M. exists w. exact/Kstar_def.satA. } case => M. move: H => /(_ M) H1 [w] H2. apply: H1. exists w. split => //=. apply/allP => s inC. apply/evalP. exact: H2. Qed.
imports: Relations Lia mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype) CompDecModal.Kstar(Kstar_def demo hilbert_ref gen_def)