Showing the function=? is impossible
Using the halting problem seems like the good solution. Suppose you have a function red that takes the code of a function (or λ-term) (or a untyped function), reduces one step (or β-redex) in it and returns the code of the resulting function. Suppose also that you have a function normal that says if the term is in normal form. 

In Turing machines language, red would be the computation of one step and normal would return true when we are in a final state.

Let's simulate the computation of $n$ steps, returning $43$ instead of $1$ if we reach the end of the computation:

(define (run t n)
  (if (= n 0) 1
    (if (normal t) 43
      (run (red t) (n-1)))))


Then we can decide if the execution of a term will terminate or not:

(define (one x) 1)
(define (terminate t) (not (function=? (run t) one)))


From that we can use the usual diagonal argument:

(define (loop x) (loop x))
(define (f x) (if (terminate (code-of-application x (quote x))) (loop 0) 1)
(f code-of-f)


If f terminates on code-of-f then (terminate (code-of-application code-of-f (quote code-of-f)) will return true and then f will loop on code-of-f. So it should loop. Then (terminate ...) should return false and f will terminate on code-of-f, contradiction.

Technicalities: one need to define a base language which is expressive enough to be able to write everything is written above. You then need red and normal which can be tougher than one can imagine. You need also the standard quine techniques: quote which, given the code of a term, returns a term representing the code of the term, code-of-application a b is easy and self-explanatory, and of course you need to write everything above internally to write code-of-f.

The lambda-calculus is surprisingly simple and expressive to both write all this down and to prove its correctness, which is why Church used it to solve Hilbert's tenth problem, but one can do it in a lot of languages, possibly in a simpler way, using language-specific quine tricks.