I'm reading Barendregt's Lambda calculi with types (1992). In Proposition 4.1.4.1., he "proves" a lemma which shows the approximation rule implies the equality rule in typed lambda-calculi à la Curry, e.g., systems of type assignments. More technically, let $\lambda\cdot \mathcal A$ be a system of typed lambda-calculus with the approximation rule, i.e., $\Gamma \vdash M : \sigma$ is derivable whenever $\Gamma \vdash P : \sigma$ is derivable for every $P \in \mathcal A(M)$, where $\mathcal A(M)$ denotes the set of approximations of the lambda term $M$. (It has also rules for $\bot$, which stands for unsolvable terms, and $\bot : \sigma$ for every $\sigma$.) Proposition 4.1.4.1 states that, conversely, if $\Gamma \vdash M : \sigma$, $\Gamma \vdash P : \sigma$ for every $P \in \mathcal A(M)$.
However, I'm not convinced by his ultra-concise "proof," which "use" the fact $\bot$ has arbitrary types, and I'm trying to prove it on my own. Obviously, I use induction on derivation of statements on types. The problem resides in function application: I don't know how to relate $\mathcal A(MN)$ with $\mathcal A(M)$ and $\mathcal A(N)$.
I'd be the most grateful if you could suggest me how to prove it.
I figured this out by myself; I write the proof (sketch) here just in case.
Suppose $\Gamma \vdash M : \sigma$ and $P \in \mathcal A(M)$. Then, there exists a lambda-term $P'$ such that $P'$ is obtained by replacing $\bot$ in $P$ with some lambda-terms $Q_1,\dots,Q_n$ and $M$ beta-reduces to $P'$. By the Subject Reduction Theorem, $\Gamma \vdash P' : \sigma$. By replacing $Q_j : \tau_j$ in the derivation of $P' :\sigma$ with $\bot : \tau_j$, we have a derivation for $\Gamma \vdash P : \sigma$. (tombstone)
Of course this proof assumes the Subjection Reduction Theorem. I don't know if this really is necessary. But I'm happy with the proof, since I doubt if it makes sense to think of type assignment systems that fail to satisfy the Subject Reduction Theorem.