proposition: Lemma auP2 w : reflect (pAU e p q w) (AUb w).
proof: Proof. Proof using serial_e. rewrite /AUb; apply: introP => [|nLfp]. - move: w. pattern (lfp (AU_fun e p q)). apply: lfp_ind; first by move => ?; rewrite inE. move => X IH w. case/setUP; rewrite !inE. + move => qw pi pi1 pi2. exists 0 => //; congruence. + case/andP => pw /forall_inP inX pi pi1 pi2. rewrite -pi2 in inX. move: (IH _ (inX _ (pi1 0)) (ptail pi)). repeat case/(_ _)/Wrap => //; first exact: path_ptail. case => m m1 m2. exists m.+1 => //. case => //; congruence. - pose e' := [rel x y | e x y && (~~ AUb x ==> p x ==> ~~ AUb y)]. have E x : exists y, e' x y. case: (boolP (AUb x)); case: (boolP (p x)) => px pAU; try by case: (serial_e x) => y xy; exists y => //= ; rewrite ?(negbTE px); bcase. move: pAU. rewrite /AUb (lfpE (AU_mono e p q)) !inE negb_or px negb_and negb_forall /=. case/andP => _ /existsP [y]. rewrite negb_imply. case/andP => *. exists y. bcase. case: (xchoose_rel E) => f Hf. pose pi n := iter n f w. have Pe': path (fun x y => e' x y) pi by move => n; move : (Hf (pi n)). suff S k : (exists2 m : nat, m < k & ~ p (pi m)) \/ ~~ AUb (pi k). apply: pAU_pER. exists pi. split => // n; first by case/andP : (Hf (pi n)). case: (S n); first tauto. rewrite /AUb (lfpE (AU_mono e p q)) !inE negb_or => /andP [/negP ? _]. tauto. elim: k => [|k IHk]; first by right. case: IHk => [[m]|AR]; first by left; exists m => //; exact: ltnW. case: (boolP (~~ p (pi k))) => [/negP|/negPn pk] ; first by left; exists k. right. move: (Pe' k). rewrite /= AR pk /=. by bcase. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert) CompDecModal.CTL(CTL_def hilbert)