Library Float.Option
Inductive
Option
(
A
:
Set
) :
Set
:=
|
Some
:
forall
x
:
A
,
Option
A
|
None
:
Option
A
.