proposition: Theorem gen_completeness C : gen C + (exists M : fmodel, sat M C).
proof: Proof. case: (@refutation_completeness (sfc C) (@closed_sfc C) C) => // [?|H]. - left. exact: (gen_of_ref (@closed_sfc C)). - right. move: H => [M] [w] Hw _. by exists M; exists w. Qed.
imports: Lia mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype) CompDecModal.K(K_def demo)