proposition: Fact DD_supp F (sfc_F : sf_closed F) (C : clause) : C \in U F -> reflect (exists M : cmodel, sat M C) (suppS (DD F) C).
proof: Proof. move => inU. apply: introP; first exact: DD_supp_sat. move => H. apply: href_sound. apply: (href_of sfc_F) => //. apply: R1 => //. exact: coref_DD. Qed.
imports: Lia mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype) CompDecModal.K(K_def demo)