proposition: Lemma AU_ind s t u : prv (t ---> u) -> prv (s ---> fAX u ---> u) -> prv ((fAU s t) ---> u).
proof: Proof. move => H1 H2. rewrite -> axAUcmp, <- (axDN u). rule ax_contraNN. apply: ERel. Intro; ApplyH axAI; first by Rev; rule ax_contraNN. rewrite {1}/Or. rewrite -> modular_hilbert.axDN. Intro. Have (fEX (~~: u)). Intro. Apply* 2. ApplyH H2. Rev. drop. apply: rNorm. exact: axDN. drop. apply: rEXn. Intro. ApplyH ERI. ApplyH axOIr. ApplyH axOIl. rewrite -> H1. Rev. exact: axI. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert) CompDecModal.CTL(CTL_def hilbert hilbert_hist)