unfold instAddInt
x y : Int
⊢ { hAdd := fun a b => instAddInt.1 a b }.1 x y = { hAdd := fun a b => instAddInt.1 a b }.1 y x
x y : Int
⊢ { hAdd := fun a b => { add := Int.add }.1 a b }.1 x y = { hAdd := fun a b => { add := Int.add }.1 a b }.1 y x