Nitpick, but it's a bit strange to say that the two_eq_two theorem looks like a function. It looks more like a constant, since it has no arguments. (Yes I know that constants are nullary functions.)

I would find the following a more convincing presentation:

    theorem x_eq_x (x:nat) : x = x := by
      rfl

    theorem 2_eq_2 : 2 = 2 := by
      exact (x_eq_x 2)

Here x_eq_x looks like a function, and in 2_eq_2's proof we apply it like a function.