blob: e47fb37ac3a4716ab4c3abdc476d74b9f1e05b4b [file] [edit]
i j : Nat
a : Array Nat
v : Nat
h₁ : i < a.size
h₂ : j < a.size
h₃ : i = j
⊢ f a i v h₁ = f a j v h₂
i j : Nat
a : Array Nat
v : Nat
h₁ : 0 + i < a.size
h₂ : j < a.size
h₃ : i = j
⊢ f a i v (Nat.zero_add i ▸ h₁) = f a j v h₂