proposition: Lemma DC_required : (forall s, prv s -> forall (M : sts) (w : M), satisfies s w) -> DC.
proof: Proof. move => snd X R ser_R x. have xm : XM by exact: XM_required. pose M := STS (fun _ _ => False) ser_R. move: (snd _ prv_ER M x). case/(dmAll xm) => pi H. rewrite-/satisfies in H. apply (nImp xm) in H. destruct H as [p1 H]. apply (nImp xm) in H. destruct H as [p2 _]. by exists pi. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert) CompDecModal.CTL(CTL_def hilbert)