proposition: Lemma EU1 (dc : DC_ X) w : cEU R P Q w -> pEU R P Q w.
proof: Proof. Proof using R_serial. elim => {w} [w Qw|w v Pw wv _ IH]. + case: (dc _ R_serial w) => f ? ?. exists f. split => //. exists 0 => //. congruence. + case: IH => f [f1 f2 [n Bn Qn]]. exists (pcons w f). split => //. apply: path_pcons => //; by rewrite f2. exists n.+1 => //. by case. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert) CompDecModal.CTL(CTL_def hilbert)