proposition: Lemma EU_ind s t u : mprv (t ---> u) -> mprv (s ---> EX u ---> u) -> mprv (EU s t ---> u).
proof: Proof. move => H1 H2. rewrite /EU. rule ax_contra. rewrite <- axDNI. apply: rAR_ind; first by rule ax_contraNN. rewrite -[~~: s ---> Bot]/(~~: ~~: s). rewrite -> axDN. rule axC. Intro. ApplyH ax_contra. rewrite <- axDNI. ApplyH H2. Qed.
imports: mathcomp(all_ssreflect) CompDecModal.libs(edone base fset induced_sym) Setoid Morphisms Relation_Definitions