Well my first guess definitely wasn't right, but I wrote up some thoughts on strict occurrences and things, and I feel pretty confident that the second guess works. Wait, no. The twelf code examples in there are totally wrong-headed. Argh. Got my quantifiers mixed up. Hmm. Yeah, but nat : type. z : nat. s : nat -> nat. tm : type. hd : type. sp : type. lam : (hd -> tm) -> tm. app : hd -> sp -> tm. nil : sp. cons : tm -> sp -> sp. coe : hd -> tm = [x] app x nil. pat : nat -> sp -> type. pat_nil : pat z nil. tm_strict : (hd -> tm) -> type. sp_strict : (hd -> sp) -> type. sp_strict_cons : sp_strict ([x] cons (M x) (S x)) <- sp_strict S. sp_strict_cons : sp_strict ([x] cons (M x) (S x)) <- tm_strict M. tm_strict_app : tm_strict ([x] app Y (S x)) <- sp_strict S. tm_strict_lam : {N : nat} tm_strict ([x] lam ([y] M x y)) <- ({y : hd} ({S : sp} pat N S -> pat (s N) (cons (coe y) S)) -> tm_strict [x] M x y). tm_strict_var : tm_strict ([x] (app x S)) <- pat N S. %query 0 0 D : tm_strict [x] (lam [y] lam [z] app x (cons (coe y) (cons (coe y) nil))). %query 0 0 D : tm_strict [x] (lam [y] lam [z] app x (cons (coe z) (cons (coe z) nil))). %query 1 1 D : tm_strict [x] (lam [y] lam [z] app x (cons (coe y) (cons (coe z) nil))). %query 1 1 D : tm_strict [x] (lam [y] lam [z] app x (cons (coe z) (cons (coe y) nil))). ... [Closing file /home/godel/sb/encoding-strictness/enc.e lf] %% OK %%