Matching defeq problem

Stream: new members

[Snir Broshi]

Hello, I tried to match on a walk

import Mathlib
def foo {G : SimpleGraph ℕ} {a b : ℕ} : G.Walk (a + 100) (b + 100) → G.Walk (a + 100) (b + 100)
  | .nil => sorry
  | .cons h p => sorry

and got the following error:

Type mismatch
  SimpleGraph.Walk.nil
has type
  SimpleGraph.Walk ?m.29 ?m.30 ?m.30
but is expected to have type
  G.Walk (a + 100) (b + 100)

I believe the problem is that it tries to unify a + 100 and b + 100 (similar to obtain rfl) and understandably fails (it works for G.Walk (a.succ) (b.succ), probably because succ is a constructor).
Is there a way to instead get heq : a + 100 = b + 100? Or some other way to make it work?