{A B : Type} (P : A + B -> Type) (f : forall b:B, P (inr b)) : forall (x:A+B), is_inr x -> P x. Proof. intros [a|b] H; [ elim H | exact (f b) ]. Defined.
Require Import HoTT.Basics. Require Import Types.Empty Types.Unit Types.Prod Types.Sigma. Require Import Types.Bool.