{F : Type u_1} →
  {G : Type u_2} →
    {H : Type u_3} →
      [inst : Add G] →
        [inst_1 : Add H] →
          {a : G} →
            {b : H} →
              [inst_2 : FunLike F G H] →
                {motive : AddConstMapClass F G H a b → Sort u} →
                  ((map_add_const : ∀ (f : F) (x : G), f (x + a) = f x + b) → motive ⋯) →
                    (t : AddConstMapClass F G H a b) → motive t