proposition: Lemma axEXAXI s t : prv (EX s ---> AX (s ---> t) ---> EX t).
proof: Proof. do 2 Intro. Have (EX (s :/\: (s ---> t))). by ApplyH axDBD. drop. rewrite -> axAC. apply: rEXn. by rule axAcase. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert) CompDecModal.CTL(CTL_def hilbert)