ext1 a
α : Sort u_1
β : Type u_2
inst✝ : DecidableEq α
f : α ⇀ β
a₁ a₂ : α
h : a₁ ≠ a₂
g₁ g₂ : β → β
⊢ update (update f a₁ g₁) a₂ g₂ = update (update f a₂ g₂) a₁ g₁
case h
α : Sort u_1
β : Type u_2
inst✝ : DecidableEq α
f : α ⇀ β
a₁ a₂ : α
h : a₁ ≠ a₂
g₁ g₂ : β → β
a : α
⊢ update (update f a₁ g₁) a₂ g₂ a = update (update f a₂ g₂) a₁ g₁ a