lambdacube-2008.12.24: pair.cube

Pair :: * -> * -> *;
Pair a b = forall (pairT::*) . (a->b->pairT) -> pairT;

PairC :: forall (a::*) (b::*) . a -> b -> Pair a b;
PairC a b x y = \ (pairT::*) (pair :: a->b->pairT) -> pair x y;

fst :: forall (a::*) (b::*) . Pair a b -> a;
fst a b p = p a (\ (x::a) (y::b) -> x);

snd :: forall (a::*) (b::*) . Pair a b -> b;
snd a b p = p b (\ (x::a) (y::b) -> y);

split :: forall (a::*) (b::*) (r::*) . (a->b->r) -> Pair a b -> r;
split a b r f p = p r f;