rw [IH]
case succ
α : Type u
lt : α → α → Bool
x : Subarray α
n : Nat
y : Array α
x✝ : Subarray α
n✝ : Nat
y✝ : Array α
h : loop.OpSpec lt (popMax lt x✝) n✝ y✝
IH : y✝ = loop lt (popMax lt x✝) n✝
⊢ y✝ = loop lt x✝ (n✝ + 1)
case succ
α : Type u
lt : α → α → Bool
x : Subarray α
n : Nat
y : Array α
x✝ : Subarray α
n✝ : Nat
y✝ : Array α
h : loop.OpSpec lt (popMax lt x✝) n✝ y✝
IH : y✝ = loop lt (popMax lt x✝) n✝
⊢ loop lt (popMax lt x✝) n✝ = loop lt x✝ (n✝ + 1)