proposition: Theorem informative_completeness t : prv (fImp t fF) + ({ M: fmodel & #|M| <= 2^(2 * sizef t) & { w: M | eval t w}}).
proof: Proof. set F := FL t. have sfc_s := @FL_closed t. case: (@pruning_completeness F _ [fset t^+]) => //. - by rewrite powersetE fsub1 flipcl_refl // FL_refl. - move => /href_of H. left. rewrite /href in H. rewrite <- H => //. apply: bigAI => u. by rewrite inE => /eqP ->. - move => H. right. move: H => [M] [w] /(_ (t^+) (fset11 _)) /= ? S. exists M; last by exists w. apply: leq_trans S _. by rewrite leq_exp2l ?leq_mul ?FL_size. Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert) CompDecModal.PDL(PDL_def demo)