{A B : Type} (z : A + B) (w : is_inr z) : inr (un_inr z w) = z. Proof. destruct z as [a|b]; simpl. - elim w. - reflexivity. Defined.
Require Import HoTT.Basics. Require Import Types.Empty Types.Unit Types.Prod Types.Sigma. Require Import Types.Bool.