Introduce the Options.tla module

[konnov]

@shonfeder has written a nice explanation of option types in the tlaplus group:

https://groups.google.com/g/tlaplus/c/XiiJ2zg_f3U/m/RJbHjVx1AQAJ

It probably makes sense to extract this example into a module called like Options.tla. This module could also introduce the default value for the UNIT type, which seems to be a common question too.

[shonfeder]

Thank you for creating the issue! I'd like to do this work, if there are no objections. It's a nice exercise to improve my TLA+ :)