remove Classical.arbitrary & (re)move introduction of Nonempty

[TentativeConvert]

• Introduce Nonempty with some easy example before the final level of Quantus.
• Explain how to use Nonempty with obtain, as already explained in the documentation of Nonempty.
• Remove Classical.arbitrary from the final level of Quantus (and thus from the whole Game).

As an alternative to the first two points, remove Nonempty altogether by spelling out the condition as an existence statement.

[TentativeConvert]

fixed by 4c35653

[TentativeConvert]

For the record:

import Mathlib

variable (A : Type) (hne : Nonempty A) (hexists : (∃ a : A, true))

example : ∃ a : A , true := by
  obtain ⟨a,ha⟩ := hexists
  use a

example : ∃ a : A , true := by
  choose a ha using hexists
  use a

example : ∃ a : A , true := by
  --choose a ha using hne fails
  obtain ⟨a⟩ := hne
  use a