theorem not_f_eq_imp_eq
    : ¬∀{α β: Type} (f : α → β) a b, f a = f b → a = b := by
  intro h
  have : 1 = 2 := h (fun _ => 0) 1 2 rfl
  contradiction

-- Counter-counterexample? (This is trivial.)
theorem eq_imp_f_eq (f : α → β) (a b : α)
    : a = b → f a = f b := by
  intro h
  rw [h]