proposition: Theorem pruning_completeness F (sfc_F : sf_closed F) C : C \in U F -> ref F C + exists2 M:fmodel, sat M C & #|{: M}| <= 2 ^ size F.
proof: Proof. move => inU. case: (boolP (suppS (DD F) C)) => H; [right|left; exact: DD_refute]. - exists (model_of (DD F)). case/hasP : H => D D1 D2. exists (SeqSub _ D1) => s /(allP D2) ?. exact: supp_eval. - rewrite card_seq_sub ?funiq // -powerset_size subset_size // /DD /=. exact: sub_trans (prune_sub _ _) (subsep). Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.Kstar(Kstar_def)