Kleene 84: {∀x:T.{A x} ⇔ ~(∃x:T.~(A x))}

This proof is interesting because this is the first encountered of Kleene's theorems that is doubly squashed - there is an outer squashing and a squashing of the inner (A x) of the ∀x.T:(A x). While we've seen that the outer squashing on the classical direction of theorems can be discarded immediately, we'll see that the inner squashing can also easily be discarded. If we have False or a squashed goal, for which both carry no evidence, we can open squashed terms in our hypotheses. Kleene theorem 85 is similar to this one.

We can use the construction rule to get down to the goal False. We can then spread the 'for all' operator in our hypotheses to give us x : T and {A x}. Since we have False as our goal, which has no evidence term, we can open the squashed term {A x} in the hypotheses because it has similar evidence. The tactic for revealing squashed hypotheses is ExposeClassical. The rest of the proof can be solved constructively without problem.

The backwards direction't can't be proved constructively. We can take off the outer squashing immediately and get down to the goal {A x}. We need to do a classical contradiction on this term because we can then apply the function f, as defined below in the second table, and instantiate x. We then have the goal ¬(A x), which we have evidence for from the classical contradiction.

Nuprl Proof