Theorem: arg_equal_implies_fn_equal_2 (MLIR/Dialects/BuiltinModel.lean)

State before:
α β γ : Type
a a' : α
b b' : β
f : α → β → γ
EQα : a = a'
EQβ : b = b'
⊢ f a b = f a' b'
Tactic:
simp [EQα, EQβ]
State after:
no goals