%query 1 *
trans empty F (app (lam [x] lam [y] x) (lam [z] z)).

%query 1 *
feval empty (app' (lam' (lam' (1 ^))) (lam' 1)) W.

%query 1 *
vtrans (clo (empty ; clo empty (lam' 1)) (lam' (1 ^))) V.

%query 2 *
trans empty F (lam [x] lam [y] app x x).