∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} [inst_1 : Nontrivial R]
  [inst_2 : WeierstrassCurve.IsElliptic W'] {x x_1 : R} (e_x : x = x_1) {y y_1 : R} (e_y : y = y_1)
  (h : W'.Equation x y), WeierstrassCurve.Affine.Point.mk h = WeierstrassCurve.Affine.Point.mk ⋯