fact: Definition is_inl_or_is_inr {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.
imports: HoTT.Basics Types.Empty Types.Unit Types.Prod Types.Sigma Types.Bool Types.Forall