% identity
%query 1 *
L : linear (lam [x] x).

% combinator K
%query 0 *
L : linear (lam [x] lam [y] x).

% combinator S
%query 0 *
L : linear (lam [x] lam [y] lam [u] app (app x u) (app y u)).

% predecessor
%query 1 *
L : linear (lam [x] case x z [x'] x').

%query 1 *
linear (lam [x] lam [y] app x y).

%query 1 *
linear (lam [x] lam [y] app y x)