id = lam [x] x.
%query 1 * of id T.
%query 1 * con' id C.
%query 1 *
P : true (exists [a:tp] exists [a1:tp] exists [a2:tp]
	    a1 == a2 & a == (a1 => a2)).

selfapp = lam [x] app x x.
%query 0 * of selfapp T.
%query 1 * con' selfapp C.
%query 0 *
P : true (exists [a:tp] exists [a1:tp] exists [a2:tp]
	    (exists [a5:tp] a1 == (a5 => a2) & a1 == a5)
	    & a == (a1 => a2)).