{A B} (z : A + B) : is_inr z -> B. Proof. destruct z as [a|b]. - intros e; elim e. - intros; exact b. Defined.
Require Import HoTT.Basics. Require Import Types.Empty Types.Unit Types.Prod Types.Sigma. Require Import Types.Bool.