proposition: Lemma dmAR (xm : XM) w : ~ cAR R P Q w -> cEU R (PredC P) (PredC Q) w.
proof: Proof. move => H. apply: (dn xm) => C. apply: H. move: w C. cofix dmAR => w Hw. have Qw : Q w. apply: (dn xm) => H. apply Hw. exact: EU0. case: (xm (P w)) => [Pw|nPw]; first exact: AR0. apply: ARs Qw _ => v wv. apply: dmAR => C. apply: Hw. exact: EUs C. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert) CompDecModal.CTL(CTL_def hilbert)