eta expansion lemma

eta_stuff.v

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

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

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

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*)
Admitted.