I'd like to emphasise a few relevant distinctions. First, as mentioned, is the various senses of "constructive". The important two here are Markov's (russian) tradition, where it is assumed that all functions are computable. The other is Bishop's tradition, where all assumptions are valid both classically and in Markov's tradition (and in other senses). So, Bishop's school does not assume that there are non-computable functions, but neither does it assume that all functions are computable.

Andrej's earlier proof is in Bishop's tradition. There are of course proofs that the computable real numbers are not computably enumerable, and other proofs that the classical real numbers are not classically enumerable. But the proof he posted is a unifying proof that the real numbers are not enumerable.

A second distinction is between the set of real numbers and the set of infinite binary sequences. A bijection exists classically, but is non-constructive. A third distinction is between these two sets, and the class of all subsets of $\mathbb{N}$. It is useful to talk about sets of natural numbers, even if their characteristic function is undecidable. For instance, the set of (codes for) lambda terms of convergent series (Cauchy sequences). This is a subset of $\mathbb{N}$, but only classically does its characteristic function exist, so only classically will it be an element of the set $2^\mathbb{N}$.

Finally, there is the distinction between countable and subcountable. A set is subcountable if it is the image of a subset of $\mathbb{N}$. Classically, every subcountable set is countable, but not so constructively. There are even simple models of CZF (a version of ZF with intuitionistic logic) where every set is subcountable (even within the model), whereas the set of real numbers, as said above, is not countable.

So, with all these in mind:

The real numbers are not countable. But there is proof, in Markov's tradition, that the real numbers are subcountable - which is basically yours, since the set of valid lambda terms is a subset of $\mathbb{N}$.

There is a diagonal argument, valid in Bishop's tradition, that $2^\mathbb{N}$ is not countable, but similarly there is a Markovian proof that $2^\mathbb{N}$ is subcountable. Finally, there is a diagonal argument, valid in Bishop's tradition, that the class of all subsets of $\mathbb{N}$ is not even subcountable.