simp
n : ℕ
p : Vector ℕ n → ℕ → ℕ
hp : Arith₁ fun v => p v.tail v.head
i : Fin n
F : Vector ℕ (n + 1) → ℕ := fun v => (p v.tail v.head).inv.or ((v.get i.succ).isLeNat v.head)
hF : Arith₁ F
this : Arith₁ fun v => v.head.isEqNat (v.get i.succ)
⊢ ∀ (i_1 : Vector ℕ (n + 1)), i_1.head.isEqNat (i_1.get i.succ) = (fun v x => x.isEqNat (v.get i)) i_1.tail i_1.head
no goals