proposition: Lemma XM_required : (forall s, prv s -> forall (M : ts) (w : M), eval 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. pose M := TS R L. exact: (@snd _ (axDN (fV 0)) M tt). Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)