fact: Definition is_inl_decompose_l {A B C} (f : C -> A + B) (z : decompose_l f) : is_inl (f (equiv_decompose f (inl z))) := z.2.
imports: HoTT.Basics Types.Empty Types.Unit Types.Prod Types.Sigma Types.Bool Types.Forall