have : Arith₁ F :=
  (Arith₁.and 0 1).comp₂ _
    ((Arith₁.le 0 1).comp₂ _ hf (proj i.succ))
    ((Arith₁.lt 0 1).comp₂ _ (proj i.succ)
      (Arith₁.comp' hf (Arith₁.cons
        ((Arith₁.add 0 1).comp₂ _ Arith₁.head one) (fun i => Arith₁.tail (proj i)))))
n : ℕ
i : Fin n
f : Vector ℕ n → ℕ → ℕ
hf : Arith₁ fun v => f v.tail v.head
F : Vector ℕ (n + 1) → ℕ :=
  fun v => ((f v.tail v.head).isLeNat (v.get i.succ)).and ((v.get i.succ).isLtNat (f v.tail (v.head + 1)))
⊢ ArithPart₁ fun v => Nat.rfind fun x => Part.some (decide (f v x ≤ v.get i ∧ v.get i < f v (x + 1)))
n : ℕ
i : Fin n
f : Vector ℕ n → ℕ → ℕ
hf : Arith₁ fun v => f v.tail v.head
F : Vector ℕ (n + 1) → ℕ :=
  fun v => ((f v.tail v.head).isLeNat (v.get i.succ)).and ((v.get i.succ).isLtNat (f v.tail (v.head + 1)))
this : Arith₁ F
⊢ ArithPart₁ fun v => Nat.rfind fun x => Part.some (decide (f v x ≤ v.get i ∧ v.get i < f v (x + 1)))