variables {α : Type} (f : α → α)def injective {α Β: Type} (f: α → β) : Prop :=  ∀ {{x y}}, f x = f y → x = y -- NOTE: weakly implicitdef injective2 {α β : Type} (f : α → β) : Prop :=    ∀ {x y}, f x = f y → x = y -- NOTE: implicitdef foo (h: injective f) : false := sorryexample (h: injective f) : false :=begin  have := @foo,  unfold injective2 at *,  exact this f henddef bar (h : injective2 f) : false := sorryexample (h : injective2 f) : false :=begin  have := @bar,  unfold injective2 at *,  exact this f hend

The error becomes:

type mismatch at application  this f hterm  hhas type  f ?m_1 = f ?m_2 → ?m_1 = ?m_2but is expected to have type  ∀ {x y : α}, f x = f y → x = y