proposition: Lemma AUH_hil (s t u v : form) : prv (u :/\: t ---> Bot) -> prv (u ---> s ---> ~~: AX (AU_ (~~: u :/\: v) s t)) -> prv (u ---> AU_ v s t ---> Bot).
proof: Proof. move => H0 H1. suff sf: prv (AU_ v s t ---> AU_ (~~: u :/\: v) s t). { do 2 Intro. Have (~~: t); [Intro; ApplyH H0; by ApplyH axAI| Intro]. Have ((s :/\: v) :/\: AX (AU_ v s t)). + Rev* 1. rewrite /AU_. rewrite -> axAUeq at 1. rewrite /Or. Intro. Apply. ApplyH axAcase. do 2 Intro. by Apply* 3. + rewrite -> sf at 2. do 2 ApplyH axAcase. do 2 Intro. by ApplyH H1. } apply: rAU_ind. - rule axAcase. do 2 Intro. ApplyH axAUI. ApplyH axAI. ApplyH axAI. Intro. ApplyH H0. by ApplyH axAI. - rule axAcase. do 3 Intro. ApplyH axAUf. ApplyH axAI. ApplyH axAI. Intro. by ApplyH H1. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype) CompDecModal.CTL(CTL_def hilbert)