proposition: Lemma axAUr (s t u : form) : prv (AR Bot (u ---> ~~:t :/\: EX u) ---> u ---> ~~: AU s t).
proof: Proof. apply: rAIL. rule ax_contra. rewrite -> axDNE. rewrite -> dmA. rewrite <- axOC. rewrite /Or. rewrite -> axDNE. set X := ~~: AR _ _. apply: rAU_ind. - rewrite /X. rewrite -> axARE. do 3 Intro. Suff (~~: t). Intro; Apply. ApplyH axAEl. by Apply. - drop. rewrite {2}/X. rewrite -> axAReq. rewrite -> dmA. rewrite -> axOF. rewrite /Or. rewrite -> axDNE. rewrite -> dmAX. rewrite -/X. do 3 Intro. ApplyH (axEXAXI u). ApplyH axAEr. by Apply. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert) CompDecModal.CTL(CTL_def hilbert)