example (h : {a b : α} → a = b) : a = b := _
