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