∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} {point : WeierstrassCurve.Jacobian.PointClass R}
  (nonsingular : W'.NonsingularLift point) (point_1 : WeierstrassCurve.Jacobian.PointClass R)
  (nonsingular_1 : W'.NonsingularLift point_1),
  ({ point := point, nonsingular := nonsingular } = { point := point_1, nonsingular := nonsingular_1 }) =
    (point = point_1)