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