induction' k with k ih
m n k : MyNat
⊢ (m.add n).add k = m.add (n.add k)
case zero
m n : MyNat
⊢ (m.add n).add zero = m.add (n.add zero)

case succ
m n k : MyNat
ih : (m.add n).add k = m.add (n.add k)
⊢ (m.add n).add k.succ = m.add (n.add k.succ)