PTS *:* (*,*,*);
let
    Int:*; 0:Int;
    #include <EqType.pts>

/*
    Absurd : * = \/ r:* . r;
    absurd : 
*/
    -- callcc (\ (k:a->b) . (e:a)) : a
--    callcc (a:*) (b:*) : ((a->b)->a)->a;

    -- if c non-empty then b->d
    decomp1 (a:*) (b:*) (c:*) (d:*) (eq:EqType (a->b) (c->d)) : c->b->d =
        let f : (b->(a->b)) -> (b->(c->d)) = eq (/\ x:* . b -> x);
	    g : b->c->d = f (\ x:b . \ y:a . x);
	    h (x:c) (y:b) : d = g y x;
	in  h;

--    lemma (a:*) (b:*) : (b->a) -> b = \ f:b->a . callcc 

    decomp2 (a:*) (b:*) (c:*) (eq:EqType (b->a) (c->a)) : a->Int =
	let x:a;
	in  0;
--        let f : (b->(a->b)) -> (b->(a->c)) = eq (/\ x:* . b -> x);
--	    g : b->a->c = f (\ x:b . \ y:a . x);
--	    h (x:a) (y:b) : c = g y x;
--	in  h;

in  *