include "Bool.ma".

include "Universes.ma".
include "Equality.ma".

ninductive Maybe (A: Type[0]): Type[0] ≝
  Nothing: Maybe A
| Just: A → Maybe A.

ndefinition is_just ≝
  λA: Type[0].
  λm: Maybe A.
    match m with
      [ Nothing ⇒ False
      | Just j ⇒ True
      ].
      
ndefinition is_nothing ≝
  λA: Type[0].
  λm: Maybe A.
    match m with
      [ Nothing ⇒ True
      | Just j ⇒ False
      ].
      
ndefinition to_maybe ≝
  λA: Type[0].
  λb: Bool.
  λa: A.
    match b with
      [ True ⇒ Just A a
      | False ⇒ Nothing A
      ].
      
nlemma to_maybe_is_just:
  ∀A: Type[0].
  ∀a: A.
  ∀b: Bool.
    is_just A (to_maybe A b a) = b.
  #A a b.
  ncases b.
  nnormalize.
  @.
  nnormalize.
  @.
nqed.