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. apply: introP => [HC | HC [inS0]]. - have inS0 : C \in S0 F. move: C HC. apply/subP. exact: prune_sub. split => //. apply: (@DD_supp_sat F). existsb C => //. rewrite suppxx //. case/sepP : inS0; bcase. - move: (coref_DD sfc_F) => /(_ C). rewrite inE HC inS0 => /(_ erefl) /href_of => H. apply: href_sound. 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)