fact: Definition not_is_inl_and_inr {A B} (P : A -> Type) (Q : B -> Type) (x : A + B) : is_inl_and P x -> is_inr_and Q x -> Empty.
imports: HoTT.Basics Types.Empty Types.Unit Types.Prod Types.Sigma Types.Bool Types.Forall