{F : Type u_10} →
  {M : Type u_11} →
    {N : Type u_12} →
      [inst : Add M] →
        [inst_1 : Add N] →
          [inst_2 : FunLike F M N] →
            {motive : AddHomClass F M N → Sort u} →
              (t : AddHomClass F M N) → ((map_add : ∀ (f : F) (x y : M), f (x + y) = f x + f y) → motive ⋯) → motive t