proposition: Lemma evalbAG (M : fmodel) (w : M) s : evalb (fAG s) w = (evalb s w && evalb (fAX (fAG s)) w).
proof: Proof. by rewrite [fAX _]lock /= /AGb (gfpE (AR_mono _ _)) inE -lock. Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype) CompDecModal.Kstar(Kstar_def)