proposition: Lemma axAUEGF s t : mprv (AU s t ---> EG (~~: t) ---> Bot).
proof: Proof. rewrite /ER. do 2 Intro. Apply. Rev. by rewrite -> (axsT s), <-(axDNI t). Qed.
imports: mathcomp(all_ssreflect) CompDecModal.libs(edone base fset induced_sym) Setoid Morphisms Relation_Definitions