∀ {F : Type u_1} [inst : Field F] {W : WeierstrassCurve.Affine F} (motive : W.Point → W.Point → Sort u_2) (P : W.Point)
  (h_1 : (P : W.Point) → motive WeierstrassCurve.Affine.Point.zero P)
  (h_2 : (P : W.Point) → motive P WeierstrassCurve.Affine.Point.zero)
  (h_3 :
    (x₁ y₁ : F) →
      (h₁ : W.Nonsingular x₁ y₁) →
        (x₂ y₂ : F) →
          (h₂ : W.Nonsingular x₂ y₂) →
            motive (WeierstrassCurve.Affine.Point.some x₁ y₁ h₁) (WeierstrassCurve.Affine.Point.some x₂ y₂ h₂)),
  (match WeierstrassCurve.Affine.Point.zero, P with
    | WeierstrassCurve.Affine.Point.zero, P => h_1 P
    | P, WeierstrassCurve.Affine.Point.zero => h_2 P
    | WeierstrassCurve.Affine.Point.some x₁ y₁ h₁, WeierstrassCurve.Affine.Point.some x₂ y₂ h₂ =>
      h_3 x₁ y₁ h₁ x₂ y₂ h₂) =
    h_1 P