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