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