Surely $x=2$ is a $Proposition$. If so, then under the correspondence of propositions as types, the above proposition has a type. Which type is it?
Additionally, under the correspondence of proofs as terms, I should also see some $\lambda-term$ as a proof of the above proposition. Can you give an example?
I was thinking the type would be $Eq(x,2,Nat)$, the equality type with terms $x$ and $2$ and type $Nat$? On the other hand, the proposition may be an assignment $x:=2$ rather than an equality. Does that change the type? Because then I would immediately think of $\lambda$-binding so the proposition would look like $\lambda x.2$. Or is that entirely unrelated?
The Curry-Howard correspondence works best for propositional logic, in which we don't consider any internal structure of atomic propositions. In other words, the formulas being considered contain only propositional variables (which can take the values "true" or "false") and logical connectives.
"$x=2$" belongs not to propositional logic, but to first-order logic, where we have variables that stand for individual mathematical objects (such as numbers) and predicates (such as $=$) that express relations between these objects.
Under the Curry-Howard correspondence, first order logic usually becomes a lambda calculus with dependent types, and things are a good deal more complicated than with the simply typed lambda calculus that works for propositional logic.
But that's not the end of your trouble here. Because $x=2$ is not always true (or at least it's not necessarily true if the universe we're speaking about contains numbers other than $2$), you have better not be able to prove it.
And since there is no proof of $x=2$, it is futile to look for a lambda term that would encode such a hypothetical proof.