%query 1 *
cmp (lam [x] pair (snd x) (fst x)) ([x] vl+ x) E.

%query 1 *
cmp (app (lam [x] pair (snd x) (fst x)) (pair z (s z))) ([x] vl+ x) E.

%query 1 *
ceval (vl+ (lam+ [x':cval] [k:cval -> cexp]
		  snd+ x' ([x1':cval] fst+ x' ([x2':cval] k (pair+ x1' x2')))))
     V.

%query 1 *
ceval 
    (app+
       (lam+ [x':cval] [k:cval -> cexp]
          snd+ x' ([x1':cval] fst+ x' ([x2':cval] k (pair+ x1' x2'))))
       (pair+ z+ (s+ z+)) ([x:cval] vl+ x))
    V.