proposition: Lemma supp_S_sat (F : clause) (sfc_F : sf_closed F) C : suppS (S F) C -> (exists M : fmodel, sat M C).
proof: Proof. move => sC. case/hasP : sC => D inSF sDC. have inDD : D \in DD F by rewrite inE inSF. exists (model_of (DD F)). exists (SeqSub _ inDD) => s inC. apply: supp_eval => /=. exact: (allP sDC). 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)