{A B} (x : A + B) (na : ~ A) : is_inr x := match x with | inl a => na a | inr b => tt end.
Require Import HoTT.Basics. Require Import Types.Empty Types.Unit Types.Prod Types.Sigma. Require Import Types.Bool.