rw [add_succ, add_succ]
case succ
a b t' : Nat
ih : a + t' = b + t' → a = b
⊢ a + succ t' = b + succ t' → a = b
case succ
a b t' : Nat
ih : a + t' = b + t' → a = b
⊢ succ (a + t') = succ (b + t') → a = b