{F : Type u_1} →
  [inst : Field F] →
    {W : WeierstrassCurve.Affine F} →
      (motive : W.Point → W.Point → Sort u_2) →
        (x x_1 : W.Point) →
          ((P : W.Point) → motive WeierstrassCurve.Affine.Point.zero P) →
            ((P : W.Point) →
                (P = WeierstrassCurve.Affine.Point.zero → False) → motive P WeierstrassCurve.Affine.Point.zero) →
              ((x₁ y₁ : F) →
                  (h₁ : W.Nonsingular x₁ y₁) →
                    (x₂ y₂ : F) →
                      (h₂ : W.Nonsingular x₂ y₂) →
                        motive (WeierstrassCurve.Affine.Point.some h₁) (WeierstrassCurve.Affine.Point.some h₂)) →
                motive x x_1