proposition: Theorem ref_compl (F C: clause) u (sfc_F : sf_closed F) (inhF : u \in F) (inU : C \in U F) : (ref F C) + (exists2 M:fmodel, #|M| <= size F * 2 ^ (2 * size F + 1) & exists w:M, forall s, s \in C -> eval (interp' s) w).
proof: Proof. case: (boolP (suppS (DD F) C)) => H; [right|left]; last exact: DD_refute. case: (fset0Vmem C) => [E|[s inC]];subst. - exists unit_model. + rewrite card_unit muln_gt0 expn_gt0 /= andbT. apply/size_gt0P. by exists u. + exists tt => s. by rewrite inE. - case/hasP : H => D D1 /allP H. move: (H _ inC)=>/suppE/emptyPn [v inD]. have inFs : v \in Fs (DD F) by apply/cupP; exists D; bcase. case: (DD_small_model inFs D1) => M ? [w Hw]. exists M => //; exists w. move => t /H. exact: Hw. Qed.
imports: Lia mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base sltype) CompDecModal.CTL(CTL_def dags demo)