The proof by Frank Fu which I mentioned in my last post was missing an important lemma: non-emptiness of the set , for all simple types . This was pointed out in a comment to that post, by Chris Casinghino. Frank has added the proof of this property to a revised version of the proof, as an additional property CR 4. The step case of the induction for CR 1 (stating that reducible terms are closed and strongly normalizing) needs to choose an element of , and so must appeal to IH(CR 4) for the fact that such an element exists.
Now the question I would want to know is, if we extended this particular proof to System F, would the reducibility candidates have to be defined as satisfying CR 4? Since this is needed for CR 1, one would presume the answer is yes. This would quite worrisome for some proofs (e.g., the one in Girard’s Proofs and Types), where is a set of terms of type — and of course, System F has types which are uninhabited in the empty context (contradicting CR 4). But in the proof Frank has done, reducible terms need not be typable. So perhaps requiring CR 4 would not be a problem.