∀ {G : Type v} {X : Type w} [inst : PseudoEMetricSpace X] [inst_1 : AddGroup G] [inst_2 : AddAction G X]
  [inst_3 : IsIsometricVAdd G X] (c : G), (IsometryEquiv.constVAdd c).toEquiv = AddAction.toPerm c