Redefine Set.Nontrivial

[urkud]

Redefine Set.Nontrivial as

protected def Set.Nontrivial (s : Set α) : Prop :=
  ∃ x ∈ s, ∃ y ∈ s, x ≠ y

which is interpreted as

protected def Set.Nontrivial (s : Set α) : Prop :=
  ∃ x, x ∈ s ∧ ∃ y, y ∈ s ∧ x ≠ y

as opposed to the current definition

protected def Nontrivial (s : Set α) : Prop :=
  ∃ (x : α) (_ : x ∈ s) (y : α) (_ : y ∈ s), x ≠ y

This change is aligned with changes we made elsewhere in the port
(sometimes accidentally, because the interpretation of ∃ x ∈ s, p x
changed).