Factor some of the uses of extensionality off into a lemma.
Some cleanup of the denotational semantics proof.