{G : Type u_1} →
  {H : Type u_2} →
    [inst : Add G] →
      [inst_1 : Add H] →
        {a : G} →
          {b : H} →
            {motive : AddConstMap G H a b → Sort u} →
              ((toFun : G → H) →
                  (map_add_const' : ∀ (x : G), toFun (x + a) = toFun x + b) →
                    motive { toFun := toFun, map_add_const' := map_add_const' }) →
                (t : AddConstMap G H a b) → motive t