proposition: Lemma axEUI s t : mprv (t ---> EU s t).
proof: Proof. rewrite /EU. rewrite -> (axDNI t) at 1. rule ax_contraNN. exact: axARE. Qed.
imports: mathcomp(all_ssreflect) CompDecModal.libs(edone base fset induced_sym) Setoid Morphisms Relation_Definitions