lambdacube-2008.12.24: either.cube

Either :: * -> * -> *;
Either a b = forall (eitherT::*) . (a->eitherT) -> (b->eitherT) -> eitherT;

Left :: forall (a::*) (b::*) . a -> Either a b;
Left a b x = \ (eitherT::*) (left::a->eitherT) (right::b->eitherT) -> left x;

Right :: forall (a::*) (b::*) . b -> Either a b;
Right a b y = \ (r::*) (left::a->r) (right::b->r) -> right y;

either :: forall (a::*) (b::*) (r::*) . (a->r) -> (b->r) -> Either a b -> r;
either a b r left right s = s r left right;