theorem ex : ∀ x : Unit, x = () := by
  intro (); rfl