proposition: Lemma AU_ind_aux s t u : prv (t ---> u) -> prv (fAX u ---> u) -> prv ((fAU s t) ---> u).
proof: Proof. move => H1 H2. rule ax_contra. rule axAUr. apply: rGen. rewrite -> H1. Intro. ApplyH axAI. Rev. rule ax_contraNN. rewrite -[fAX _]/(AX (~~: (~~: u))). by rewrite -> axDNE. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert) CompDecModal.CTL(CTL_def hilbert)