proposition: Lemma ARH_hil (s t C H : form) : prv (t ---> ~~: C) -> prv (EX (EU_ (~~: C :/\: H) s t) ---> s ---> ~~: C) -> prv (C ---> EU_ H s t ---> fF).
proof: Proof. move => H0 H1. suff sf: prv (EU_ H s t ---> EU_ (~~: C :/\: H) s t). { do 2 Intro. Have (~~: t); [Intro; ApplyH H0; by ApplyH axAI| Intro]. Have ((s :/\: H) :/\: EX (EU_ H s t)). + Rev* 1. rewrite /EU_. rewrite -> axEUeq at 1. rewrite /Or. Intro. Apply. ApplyH axAcase. do 2 Intro. by Apply* 3. + rewrite -> sf at 2. do 2 ApplyH axAcase. do 3 Intro. by ApplyH H1. } apply: EU_ind. - rule axAcase. do 2 Intro. ApplyH axEUI. ApplyH axAI. ApplyH axAI. Intro. by ApplyH H0. - rule axAcase. do 3 Intro. ApplyH axEUI2. 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)