In Idris, can I prove free theorems, e.g. the only (total) function of type `forall t. t -> t` is `id`?

For sufficiently polymorphic types, parametricity can uniquely determine the function itself (see Wadler's Theorems for free! for details). For example, the only total function with type forall t. t -> t is the identity function id.

Is it possible to state and prove this in Idris? (And if it can't be proven inside Idris, is it true anyway?)

The following is my attempt (I know that function equality is not a primitive concept in Idris, so I assert that any function of generic type t -> t always returns the same result as the identity function would return):

%default total

GenericEndomorphism: Type
GenericEndomorphism = (t: Type) -> (t -> t)

id_is_an_example : GenericEndomorphism
id_is_an_example t = id

id_is_the_only_example : (f : GenericEndomorphism) -> (t : Type) -> (x : t) -> f t x = x
id_is_the_only_example f t x = ?id_is_the_only_example_rhs

The resulting hole is:

- + Main.id_is_the_only_example_rhs [P]
 `--                                f : GenericEndomorphism
                                    t : Type
                                    x : t
     -------------------------------------------------------
      Main.id_is_the_only_example_rhs : f t x = x