proposition: Lemma DD_supp_sat F C : suppS (DD F) C -> exists M : cmodel, sat M C.
proof: Proof. case/hasP => D inDD /allP H. exists (model_of (DD F)). exists (Sub D inDD) => s inC. apply: supp_eval. exact: H. Qed.
imports: Lia mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype) CompDecModal.K(K_def demo)