proposition: Lemma XM_required : (forall s, prv s -> forall (M : sts) (w : M), satisfies s w) -> XM.
proof: Proof. move => snd. suff S : (forall P, ~ ~ P -> P). move => P. apply: S => C. apply: (C). right => p. apply C. by left. move => P. pose L (p : var) (w :unit) := P. pose R (w v : unit) := True. have ser x : exists y, R x y. by exists tt. pose M := STS L ser. exact: (@snd _ (axDN (fV 0)) M tt). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert) CompDecModal.CTL(CTL_def hilbert)