proposition: Lemma AU1 w : cAU R P Q w -> pAU R P Q w.
proof: Proof. elim => {w} [w Qw|w Pw _ IH]. - move => f _ f2. exists 0; by [|congruence]. - move => f pf f0. rewrite -f0 in IH. case: (IH _ (pf 0) (ptail f)) => // [|n n1 n2]. exact: path_ptail. exists n.+1 => //. case => [|k]. congruence. exact: n1. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert) CompDecModal.CTL(CTL_def hilbert)