Library MenhirLib.Tuples

From Coq Require Import List Syntax Equality.

Definition arrows_left: list Type -> Type -> Type :=
  fold_left (fun A B => B -> A).

Definition arrows_right: Type -> list Type -> Type :=
  fold_right (fun A B => A -> B).

Fixpoint tuple (types : list Type) : Type :=
  match types with
  | nil => unit
  | t::q => prod t (tuple q)
  end.

Fixpoint uncurry {args:list Type} {res:Type}:
  arrows_left args res -> tuple args -> res :=
  match args return forall res, arrows_left args res -> tuple args -> res with
    | [] => fun _ f _ => f
    | t::q => fun res f p => let (d, t) := p in
      (@uncurry q _ f t) d
  end res.

Lemma JMeq_eqrect:
  forall (U:Type) (a b:U) (P:U -> Type) (x:P a) (e:a=b),
    eq_rect a P x b e ~= x.
Proof.
destruct e.
reflexivity.
Qed.