proposition: Lemma axERu s t : mprv (ER s t ---> t :/\: (s :\/: EX (ER s t))).
proof: Proof. rule ax_contra. rewrite /ER. rewrite <- axDNI, dmA, dmO. rewrite /EX. do ! rewrite -> axDN. rule axOE. exact: axAUI. rule axAcase. exact: axAUf. Qed.
imports: mathcomp(all_ssreflect) CompDecModal.libs(edone base fset induced_sym) Setoid Morphisms Relation_Definitions