solution to eta problem

eta_sol.v

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.

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.

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

Lemma univ_conj_commute{X}(P Q : X -> Prop) : (forall x, P x /\ Q x) -> (forall x, P x) /\ (forall x, Q x).
Proof.
  firstorder.
Qed.

Lemma nice_ee_aux : forall ts t, (forall X, @nice X _ (etaexpand ts t)) /\ forall f, etaexpand ts t f = f.
Proof.
  induction ts; unfold nice; simpl.
  auto.
  intros.
  unfold nice in IHts.
  split.
  intros.
  destruct (univ_conj_commute _ _ IHts).
  rewrite H0.
  auto.
  apply H1.
  intros.
  destruct (univ_conj_commute _ _ IHts).
  apply H.
  apply H0.
Qed.

Lemma etaexpand_id : forall ts t f, etaexpand ts t f = f.
Proof.
  intros.
  destruct (univ_conj_commute _ _ (nice_ee_aux ts)).
  apply H0.
Qed.