proposition: Lemma ER1 (xm : XM ) (dc : DC_ X) w : cER R P Q w -> pER R P Q w.
proof: Proof. Proof using R_serial. move => H. pose R' x y := R x y /\ (cER R P Q x -> ~ P x -> cER R P Q y). have R'_serial x : exists y, R' x y. case: (xm (cER R P Q x)); case: (xm (P x)); try by case: (R_serial x) => y; exists y. move => nPx [//|y]. by exists y. case: (dc _ R'_serial w) => f f0 pf. exists f. split => //; first by move => n; apply pf. suff S n : cER R P Q (f n) \/ (exists2 k : nat, k < n & P (f k)). move => n. case (S n);[ case; tauto|tauto]. elim: n => [|n [IHn|IHn]]; first by rewrite f0; tauto. - case: (xm (P (f n))) => HP; [right; by exists n|left]. case: (pf n) => _. by apply. - right. case: IHn => k ? ?. exists k => //. exact: ltnW. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert) CompDecModal.CTL(CTL_def hilbert)