induction b with d hd
        rw [add_zero, zero_add]
        rfl
        rw [add_succ, succ_add]
        rw [hd]
        rfl

i really enjoyed finally internalizing dependent type theory. it helped a lot with that.