Suppose we don't know Joe B. Wells's result from 1994 that both typability and type checking are undecidable in System F (AKA $\lambda 2$). In Barendregt's Lambda calculi with types (1992) I found a proof due to Malecki 1989 that type checking implies typability. This is because
exists $\sigma$ such that $M:\sigma$
is equivalent to
$(\lambda xy.y)M : (\alpha\rightarrow\alpha)$
(This is because if a term is typable in System F then all its subterms are.)
Is there a simple proof the other way around? That is, a proof that typability implies type checking in System F?