Lemma rtoneq {X : UU} {R : hrel X} (is : isirrefl R) {a b : X} (r : R a b) : a != b. Proof. intros. intro e. rewrite e in r. apply (is b r). Defined.
Require Import UniMath.Foundations.UnivalenceAxiom.