proposition: Lemma ARel s t u : prv (u ---> t :/\: (s :\/: AX (AR (s :\/: u) (t :\/: u)))) -> prv (u ---> AR s t).
proof: Proof. move => H. rewrite <- (axDNE (AR s t)), dmAR. rewrite -> (axAsT (~~: s)), (axAsT (~~: t)). apply: ARH_hil. - rule ax_contraNN. rule axB; last apply H. exact: axAEl. - rewrite /EU_. rewrite <- axAsT. do ! rewrite <- dmO. rewrite <- dmAR. rewrite /EX. rewrite -> axDNE. do 2 Intro. rewrite -> H at 3. ApplyH axAcase. Intro. by ApplyH axOE. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert) CompDecModal.CTL(CTL_def hilbert hilbert_hist)