How to prove this lemma about eta expansion?

Question

(here is a gist of my work so far.)

Coq comes with a rule about eta reduction, allowing us to prove something like the following:

Variables X Y Z : Type.
Variable f : X -> Y -> Z.

Lemma eta1 : (fun x => f x) = f.
Proof.
  auto.
Qed.

The eta rule is not merely an equality rewrite, so we can use it beneath binders as well:

Lemma eta2 : (fun x y => f x y) = f.
Proof.
  auto.
Qed.

Of course, one would expect that you could generalize this to an f of arbitrary arity. Here is my naïve attempt:

Require Import Coq.Lists.List.
Import ListNotations.

Fixpoint toType(ts : list Type)(t : Type) : Type :=
  match ts with
  |[]    => t
  |u::vs => u -> (toType vs t)
  end.

Compute toType [X;Y] Z.

(*
     = X -> Y -> Z
     : Type
*)

Fixpoint etaexpand(ts : list Type) : forall t : Type, toType ts t -> toType ts t :=
  match ts as ts return forall t, toType ts t -> toType ts t with
  |[]    => fun t x => x
  |u::vs => fun t f (x:u) => etaexpand vs t (f x)
  end.

Compute etaexpand [X;Y] Z f.
(*
     = fun (x : X) (x0 : Y) => f x x0
     : toType [X; Y] Z
*)

Lemma etaexpand_id : forall ts t f, etaexpand ts t f = f.
Proof.
  induction ts; intros.
  auto.
  simpl.
  (*stuck here*)

I get stuck on the inductive step of the above lemma. Naturally, I want to rewrite using the inductive hypothesis, but I cannot since the relevant subterm occurs beneath a binder. Of course, I myself know that the inductive hypothesis should be usable beneath binders, since it's just a chain of eta rewrites. I'm wondering then if there's a clever way to state and convince Coq of this fact.

Answer 1

In case anyone's curious, here's the solution I came up with after some thought.

The key is to simultaneously prove the following "niceness" property for etaexpand ts t:

Definition nice{X Y}(F : Y -> Y) := (forall y, F y = y) -> forall f : X -> Y, 
  (fun x => F (f x)) = f.