Idris lambdas vs. partially applied equational functions

ChurchLambda.idr

||| Church numerals using explicit lambdas, vs. equational style.  This is
||| a somewhat contrived example to demonstrate how proofs of function
||| equality can succeed for lambdas and fail for equational functions, even
||| though (to a casual observer) there isn't really a difference between the
||| two.
module ChurchLambda

-- Because I like the same names as the Prelude.  I admit I don't really
-- understand why names defined in this module don't just "win", but that's
-- not the point of this gist.  Keep scrolling.
%hide Nat
%hide succ
%hide plus
%hide mult
%hide exp

||| Church style definition of natural numbers in terms of function
||| application.
Nat : Type -> Type
Nat X = (X -> X) -> X -> X

||| Zero ignores its function and returns the second argument.  This is
||| written using an explicit lambda, instead of the more natural style.
zero : Nat t
zero = \_, x => x

||| One applies the function once; using explicit lambda.
one : Nat t
one = \f, x => f x

||| One expressed using equational style.  Seems pretty much equivalent
||| to the explicit lambda, but isn't.
one' : Nat t
one' f x = f x

||| The successor to a number involves one more function application than
||| the number.
succ : Nat t -> Nat t
succ n = \f, x => f (n f x)

||| Proving a simple property...
succ_1 : succ zero = one
succ_1 = Refl

||| This one's harder.
succ_1' : succ zero = one'
succ_1' = ?succ_1'_rhs

Okay, but why is that the case?