@[specialize]
def isEqvAux (a b : Array α) (hsz : a.size = b.size) (p : α → α → Bool) (i : Nat) : Bool :=
  if h : i < a.size then
     have : i < b.size := hsz ▸ h
     p a[i] b[i] && isEqvAux a b hsz p (i+1)
  else
    true
termination_by a.size - i
decreasing_by simp_wf; decreasing_trivial_pre_omega

theorem eq_of_isEqvAux [DecidableEq α] (a b : Array α) (hsz : a.size = b.size) (i : Nat) (hi : i ≤ a.size) (heqv : isEqvAux a b hsz (fun x y => x = y) i) : ∀ (j : Nat) (hl : i ≤ j) (hj : j < a.size), a[j] = b[j] := by
  intro j low high
  by_cases h : i < a.size
  · unfold isEqvAux at heqv
    simp [h] at heqv
    have hind := eq_of_isEqvAux a b hsz (i+1) (Nat.succ_le_of_lt h) heqv.2
    by_cases heq : i = j
    · subst heq; exact heqv.1
    · exact hind j (Nat.succ_le_of_lt (Nat.lt_of_le_of_ne low heq)) high
  · have heq : i = a.size := Nat.le_antisymm hi (Nat.ge_of_not_lt h)
    subst heq
    exact absurd (Nat.lt_of_lt_of_le high low) (Nat.lt_irrefl j)
termination_by _ _ _ => a.size - i

@[simp] def f (x y : Nat) : Nat → Nat :=
  if h : x > 0 then
    fun z => f (x - 1) (y + 1) z + 1
  else
    (· + y)
termination_by x

#check f.eq_1