badIhName.lean:13:2-13:6: error: unsolved goals
case z
⊢ add Nat.z Nat.z = Nat.z

case s
a✝ : Nat
a_ih✝ : add Nat.z a✝ = a✝
⊢ add Nat.z a✝.s = a✝.s