(datatype union

  X : A;
  ___________________
  X : (- (union A B));

  X : B;
  ___________________
  X : (- (union A B));

  X : A >> P;
  X : B >> P;
  _________________________
  X : (- (union A B)) >> P;)