proposition: Lemma ERel (s t u : form) : prv (u ---> t :/\: (s :\/: EX (ER (s :\/: u) (t :\/: u)))) -> prv (u ---> ER s t).
proof: Proof. move => H. rewrite /ER. rewrite -> (axAsT (~~: s)), (axAsT (~~: t)). apply: AUH_hil. - rule axAcase. rewrite -[~~: t ---> _]/(~~: (~~: t)). rewrite -> axDNE. rule axB; last apply H. exact: axAEl. - rewrite /AU_. rewrite <- axAsT. do ! rewrite <- dmO. rewrite <- dmER. rewrite -> H at 1. exact: axAEr. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert) CompDecModal.CTL(CTL_def hilbert hilbert_hist)