Lemma isInjective_inr {A B : UU} : isInjective (@inr A B). Proof. intros ? ?. refine (isweqinvmap (@paths_inr_inr_equiv _ _ _ _)). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.Tactics.