proposition: Lemma EU2 w : pEU R P Q w -> cEU R P Q w.
proof: Proof. case => f [f1 f2 [n n1 n2]]. elim: n w f f1 f2 n1 n2 => [w f _ -> _|n IH w f f1 f2 n1 n2]; first exact: EU0. rewrite -f2. apply: EUs (f1 0) _. exact: n1. apply: (IH _ (ptail f)) => //. exact: path_ptail. move => k. rewrite -ltnS. exact: n1. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert) CompDecModal.CTL(CTL_def hilbert)