proposition: Lemma pARE1 w : pAR e p q w -> q w.
proof: Proof. Proof using serial_e. case: (xchoose_rel serial_e) => f Hf. have pth: path e (fun n => iter n f w) by move => m; exact: Hf. move => Hw. case: (Hw (fun n => iter n f w) pth (erefl _) 0) => //. by case. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert) CompDecModal.CTL(CTL_def hilbert)