proposition: Lemma gen_completeness C : gen (C,aVoid) + (exists M : fmodel, sat M C).
proof: Proof. have sfc_F := @closed_sfc C. case (boolP (suppS (S (sfc C)) C)) => H. - right. exact: supp_S_sat H. - left. apply: refpred_tref (sfc_F) _ _. apply: S_refute => //. by rewrite powersetE sub_sfc. 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)