∀ (v : Fin2 (2 + 1) → ℕ)
  (motive :
    (∃ w a t z,
        ∃ (a1 : 1 < a),
          Pell.xn a1 ((v ∘ Fin2.fs) (Fin2.ofNat' 1)) ≡
              Pell.yn a1 ((v ∘ Fin2.fs) (Fin2.ofNat' 1)) * (a - (v ∘ Fin2.fs) (Fin2.ofNat' 0)) + v Fin2.fz [MOD t] ∧
            2 * a * (v ∘ Fin2.fs) (Fin2.ofNat' 0) =
                t + ((v ∘ Fin2.fs) (Fin2.ofNat' 0) * (v ∘ Fin2.fs) (Fin2.ofNat' 0) + 1) ∧
              v Fin2.fz < t ∧
                (v ∘ Fin2.fs) (Fin2.ofNat' 0) ≤ w ∧
                  (v ∘ Fin2.fs) (Fin2.ofNat' 1) ≤ w ∧ a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1) →
      Prop)
  (x :
    ∃ w a t z,
      ∃ (a1 : 1 < a),
        Pell.xn a1 ((v ∘ Fin2.fs) (Fin2.ofNat' 1)) ≡
            Pell.yn a1 ((v ∘ Fin2.fs) (Fin2.ofNat' 1)) * (a - (v ∘ Fin2.fs) (Fin2.ofNat' 0)) + v Fin2.fz [MOD t] ∧
          2 * a * (v ∘ Fin2.fs) (Fin2.ofNat' 0) =
              t + ((v ∘ Fin2.fs) (Fin2.ofNat' 0) * (v ∘ Fin2.fs) (Fin2.ofNat' 0) + 1) ∧
            v Fin2.fz < t ∧
              (v ∘ Fin2.fs) (Fin2.ofNat' 0) ≤ w ∧
                (v ∘ Fin2.fs) (Fin2.ofNat' 1) ≤ w ∧ a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1),
  (∀ (w a t z : ℕ) (a1 : 1 < a)
      (h :
        Pell.xn a1 ((v ∘ Fin2.fs) (Fin2.ofNat' 1)) ≡
            Pell.yn a1 ((v ∘ Fin2.fs) (Fin2.ofNat' 1)) * (a - (v ∘ Fin2.fs) (Fin2.ofNat' 0)) + v Fin2.fz [MOD t] ∧
          2 * a * (v ∘ Fin2.fs) (Fin2.ofNat' 0) =
              t + ((v ∘ Fin2.fs) (Fin2.ofNat' 0) * (v ∘ Fin2.fs) (Fin2.ofNat' 0) + 1) ∧
            v Fin2.fz < t ∧
              (v ∘ Fin2.fs) (Fin2.ofNat' 0) ≤ w ∧
                (v ∘ Fin2.fs) (Fin2.ofNat' 1) ≤ w ∧ a * a - ((w + 1) * (w + 1) - 1) * (w * z) * (w * z) = 1),
      motive ⋯) →
    motive x