have : Arith₁ F :=
  (or 0 1).comp₂ _
    ((equal 0 1).comp₂ _ ((add 0 1).comp₂ _ head (proj j.succ)) (proj i.succ))
    ((and 0 1).comp₂ _ ((lt 0 1).comp₂ _ (proj i.succ) (proj j.succ)) ((equal 0 1).comp₂ _ head zero))
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ :=
  fun v =>
    ((v.head + v.get j.succ).isEqNat (v.get i.succ)).or (((v.get i.succ).isLtNat (v.get j.succ)).and (v.head.isEqNat 0))
⊢ Arith₁ fun v => v.get i - v.get j
n : ℕ
i j : Fin n
F : Vector ℕ (n + 1) → ℕ :=
  fun v =>
    ((v.head + v.get j.succ).isEqNat (v.get i.succ)).or (((v.get i.succ).isLtNat (v.get j.succ)).and (v.head.isEqNat 0))
this : Arith₁ F
⊢ Arith₁ fun v => v.get i - v.get j