have ihl : a + t' = b + t' := by exact (succ_inj h)
case succ
a b t' : Nat
ih : a + t' = b + t' → a = b
h : succ (a + t') = succ (b + t')
⊢ a = b
case succ
a b t' : Nat
ih : a + t' = b + t' → a = b
h : succ (a + t') = succ (b + t')
ihl : a + t' = b + t'
⊢ a = b