Detect changes between implicit and explicit arguments

[urkud]

Reported on Zulip by @chrisflav.

Minimal example:

theorem foo (α β : Type) (a b : α) (f : α → β) (h : a = b) : f a = f b :=
  congrArg f h

vs

theorem foo {α β : Type} (a b : α) (f : α → β) (h : a = b) : f a = f b :=
  congrArg f h

should be shown as different.