Observational Equivalence of open terms in PCF

Question

The notion of observational equivalence is rather intuitive, but formally I'm having some doubts in the particular case of open terms.

Lets consider the simple case where the terms M and N are free variables, M = x and N = y. Choosing the program context C[-] = (λxy.[-]) v w we have,
C[M] = (λxy.x) v w →* v
C[N] = (λxy.y) v w →* w
So by definition M and N wouldn't be observationally equivalent.

However, consider any adequate denotational semantics of PCF. Then by definition of adequacy, ⟦M⟧ = ⟦N⟧ implies M and N observationally equivalent. The denotations of both (open) terms are,
⟦M⟧ = ⟦x ⊢ x⟧ = id
⟦N⟧ = ⟦y ⊢ y⟧ = id
From what we conclude M and N to be observationally equivalent.

So, surely I must be going wrong somewhere, and I suspect it to be some trivial mistake. But where?

Answer 1

Got the answer, thanks to jonsterling on reddit for the insight.

The error is that both M and N written as full judgements, must be weakened to have the same environment, and one that fits C[-]. So the question becomes whether ⟦M⟧ = ⟦x,y ⊢ x⟧ and ⟦N⟧ = ⟦x,y ⊢ y⟧ are observationally equivalent. And the contradiction above disappears.