Maybe package contains inductive data type definition representing value container with optional empty constructor.
data maybe (A: U) = nothing | just (a: A)
nothing is basic maybe point constructor.
null: maybe nat = nothing
just is maybe value wrapper.
wrapped: maybe nat = just one
maybe (A B: U) (n: B) (j: A -> B) : maybe A -> B
Returns a function from wrapped to raw values.
> maybe_ nat nat zero (\ (x: nat) -> x) (just zero)