mmasdeu

/-
Here goes the text that will appear in the main window. You can use unicode symbols like ⊢ or ∩. It is
typeset using markdown, so use *this* for emphasis, or `this` for code.
-/

/- Hint : (here goes the text for the hint box).
The text written here will be hidden until the player clicks on the hint box.
-/

variables {X : Type} -- hide <- the `hide` keyword means that this line will be hidden in the game, to unclutter.