not_is_inl_and_inr' {A B} (x : A + B) : is_inl x -> is_inr x -> Empty := not_is_inl_and_inr (fun _ => Unit) (fun _ => Unit) x.
Require Import HoTT.Basics. Require Import Types.Empty Types.Unit Types.Prod Types.Sigma. Require Import Types.Bool.