proposition: Lemma sat_hist0 (M : fmodel) (w : M) s : ~~ evalb (fAG s) w -> hist fset0 s w.
proof: Proof. rewrite /= /AGb inE negbK. move: w. apply lfp_ind; first by move => ?;rewrite inE. move => A IH w. rewrite !inE negb_and. case/orP; first (apply: hist0; exact: dsat0). case/forall_inPn => v wv. rewrite inE negbK => inA. apply: histS wv _. apply dsat0. exact: IH. Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype) CompDecModal.Kstar(Kstar_def)