proposition: Lemma rER_ind u s t : mprv (u ---> t) -> mprv (u ---> ~~: s ---> EX u) -> mprv (u ---> ER s t).
proof: Proof. move => H0 H1. rewrite /ER. rule ax_contra. rewrite -> axDN. apply: rAU_ind. by rewrite -> H0. do 3 Intro. by ApplyH H1. Qed.
imports: mathcomp(all_ssreflect) CompDecModal.libs(edone base fset induced_sym) Setoid Morphisms Relation_Definitions