proposition: Lemma axEUr s t u : prv (AR Bot (u ---> ~~:t :/\: (s ---> fAX u)) ---> u ---> ~~: EU s t).
proof: Proof. rewrite /EU. rewrite -> axDNE. apply rAIL. apply: modular_hilbert.rAR_ind. - rewrite -> axARE. rule axAcase. do 2 Intro. ApplyH axAEl. by Apply* 1. - rewrite -> axAReq at 1. rewrite -> axOF. do 2 rule axAcase. do 4 Intro. rewrite <- axABBA. ApplyH axAI. Rev. rewrite -[~~: s ---> Bot]/(~~: (~~: s)). rewrite -> axDNE. ApplyH axAEr. Apply* 2. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert) CompDecModal.CTL(CTL_def hilbert)