Maybe[T:TYPE] : THEORY
BEGIN

  Maybe: DATATYPE 
  BEGIN
    None : none?
    Some(val:T): some?
  END Maybe

  val2some(t:T) : MACRO Maybe = Some(t)

  CONVERSION val2some
 
  a : VAR Maybe

  Maybe_none : LEMMA
    none?(a) IFF
    a = None

  Maybe_some : LEMMA
    some?(a) IMPLIES
    EXISTS (t:T) : val(a) = t AND a = Some(t)

  Maybe_or : LEMMA
    none?(a) OR some?(a)

  Maybe_either: LEMMA
    a = None OR EXISTS (t:T) : val(a) = t AND a = Some(t)

END Maybe