proposition: Fact DD_canonical F (sfc_F : sf_closed F) (C : clause) : reflect (C \in S0 F /\ exists M : cmodel, sat M C) (C \in DD F).
proof: Proof. exact: DD_canonical. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset modular_hilbert base sltype) CompDecModal.K(K_def demo hilbert_ref gentzen universal_model)