α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β → γ
x : α
y : β
⊢ f x y = f x y
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β → γ
x x' : α
y y' : β
hx : x = x'
hy : y = y'
⊢ f x y = f x' y'
subst hx hy
no goals
α : Sort u_1
β : Sort u_2
γ : Sort u_3
f : α → β → γ
x : α
y : β
⊢ f x y = f x y
rfl