proposition: Lemma arP2 w : reflect (pAR e p q w) (ARb w).
proof: Proof. Proof using serial_e. apply: (iffP arP). - move => H pi p1 p2. suff S n : (exists2 m : nat, m < n & p (pi m)) \/ cAR e p q (pi n). move => n. case: (S n); first tauto. by case; right. elim: n => [|n IHn]; first by right; congruence. case: IHn => [[m]|]; first by left; exists m => //; exact: ltnW. case => [? ?|qn CI]; first by left; exists n. right. apply CI. exact: p1. - move: w. cofix arP2 => w Hw. case: (boolP (p w)) => Hp. * apply: AR0. exact: Hp. exact: pARE1. * apply: ARs => [|v wv]. exact: pARE1. apply: arP2. exact: pARE2 wv. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert) CompDecModal.CTL(CTL_def hilbert)