{A B} (P : A -> Type) (Q : B -> Type) (x : A + B) : is_inl_and P x -> is_inr_and Q x -> Empty. Proof. destruct x as [a|b]; simpl. - exact (fun _ e => e). - exact (fun e _ => e). Defined.
Require Import HoTT.Basics. Require Import Types.Empty Types.Unit Types.Prod Types.Sigma. Require Import Types.Bool.