data Maybe {a} (A : Set a) : Set a where
  just    : (x : A) -> Maybe A
  nothing : Maybe A