fact: Definition is_inr_decompose_r {A B C} (f : C -> A + B) (z : decompose_r f) : is_inr (f (equiv_decompose f (inr z))) := z.2.
imports: HoTT.Basics Types.Empty Types.Unit Types.Prod Types.Sigma Types.Bool Types.Forall