Require Import Coq.Lists.List.
Require Import Relations RelationClasses.
Require Import ExtLib.Core.Type.
Require Import ExtLib.Core.RelDec.
Require Import ExtLib.Structures.Proper.
Require Import ExtLib.Data.SigT.
Require Import ExtLib.Data.Member.
Require Import ExtLib.Data.ListNth.
Require Import ExtLib.Data.Option.
Require Import ExtLib.Tactics.
Require Import Coq.Classes.Morphisms.

Set Implicit Arguments.
Set Strict Implicit.
Set Asymmetric Patterns.
Set Universe Polymorphism.
Set Printing Universes.

(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
Lemma app_ass_trans@{X}
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
: forall {T : Type@{X} } (a b c : list T), (a ++ b) ++ c = a ++ b ++ c.
Proof.
(* Goal: forall (T : Type@{Var(0)}) (a : list T), @eq (list T) (@app T a (@nil T)) a *)
  induction a; simpl.
(* Goal: @eq (G t) (@hlist_hd A G t ls (@hlist_map A F G ff (@cons A t ls) (@Hcons A F t ls (@hlist_hd A F t ls hl) (@hlist_tl A F t ls hl)))) (@ff t (@hlist_hd A F t ls (@Hcons A F t ls (@hlist_hd A F t ls hl) (@hlist_tl A F t ls hl)))) *)
  reflexivity.
(* Goal: @eq (G t) (@hlist_hd A G t ls (@hlist_map A F G ff (@cons A t ls) (@Hcons A F t ls (@hlist_hd A F t ls hl) (@hlist_tl A F t ls hl)))) (@ff t (@hlist_hd A F t ls (@Hcons A F t ls (@hlist_hd A F t ls hl) (@hlist_tl A F t ls hl)))) *)
  intros. destruct (IHa b c). reflexivity.
Defined.

Lemma app_nil_r_trans : forall {T : Type} (a : list T), a ++ nil = a.
Proof.
(* Goal: forall (T : Type@{Var(0)}) (a : list T), @eq (list T) (@app T a (@nil T)) a *)
  induction a; simpl.
(* Goal: @eq (G t) (@hlist_hd A G t ls (@hlist_map A F G ff (@cons A t ls) (@Hcons A F t ls (@hlist_hd A F t ls hl) (@hlist_tl A F t ls hl)))) (@ff t (@hlist_hd A F t ls (@Hcons A F t ls (@hlist_hd A F t ls hl) (@hlist_tl A F t ls hl)))) *)
  reflexivity.
  refine match IHa in _ = X return _ = _ :: X with
         | eq_refl => eq_refl
         end.
Defined.

Monomorphic Universe hlist_large.

(** Core Type and Functions **)
Section hlist.
  Polymorphic Universe Ui Uv.

  Context {iT : Type@{Ui}}.
  Variable F : iT -> Type@{Uv}.

  Inductive hlist : list iT -> Type :=
  | Hnil  : hlist nil
  | Hcons : forall l ls, F l -> hlist ls -> hlist (l :: ls).

(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
  Definition hlist_hd {a b} (hl : hlist (a :: b)) : F a :=
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
    match hl in hlist x return match x return Type@{Uv} with
                               | nil => unit
                               | l :: _ => F l
                               end with
    | Hnil => tt
    | Hcons _ _ x _ => x
    end.

(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
  Definition hlist_tl {a b} (hl : hlist (a :: b)) : hlist b :=
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
    match hl in hlist x return match x return Type@{hlist_large} with
                                 | nil => unit
                                 | _ :: ls => hlist ls
                               end with
      | Hnil => tt
      | Hcons _ _ _ x => x
    end.

  Lemma hlist_eta : forall ls (h : hlist ls),
    h = match ls as ls return hlist ls -> hlist ls with
        | nil => fun _ => Hnil
        | a :: b => fun h => Hcons (hlist_hd h) (hlist_tl h)
        end h.
  Proof.
(* Goal: forall _ : @hlist_hrel A F G R (@app A (@cons A l ls0) ls) (@hlist_app A F (@cons A l ls0) ls (@Hcons A F l ls0 f x) xs) (@hlist_app A G (@cons A l ls0) ls (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y)) ys), and (@hlist_hrel A F G R (@cons A l ls0) (@Hcons A F l ls0 f x) (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y))) (@hlist_hrel A F G R ls xs ys) *)
    intros. destruct h; auto.
  Qed.

  Fixpoint hlist_app ll lr (h : hlist ll) : hlist lr -> hlist (ll ++ lr) :=
    match h in hlist ll return hlist lr -> hlist (ll ++ lr) with
    | Hnil => fun x => x
    | Hcons _ _ hd tl => fun r => Hcons hd (hlist_app tl r)
    end.

  Lemma hlist_app_nil_r
  : forall ls (h : hlist ls),
      hlist_app h Hnil =
      match eq_sym (app_nil_r_trans ls) in _ = t return hlist t with
      | eq_refl => h
      end.
  Proof.
(* Goal: forall (ls : list iT) (h : hlist ls), @eq (hlist (@app iT ls (@nil iT))) (@hlist_app ls (@nil iT) h Hnil) match @eq_sym (list iT) (@app iT ls (@nil iT)) ls (@app_nil_r_trans iT ls) in (eq _ t) return (hlist t) with | eq_refl => h end *)
    induction h; simpl; intros; auto.
(* Goal: @eq (hlist (@cons iT l (@app iT ls (@nil iT)))) (@Hcons l (@app iT ls (@nil iT)) f (@hlist_app ls (@nil iT) h Hnil)) match @eq_sym (list iT) (@cons iT l (@app iT ls (@nil iT))) (@cons iT l ls) match @app_nil_r_trans iT ls in (eq _ X) return (@eq (list iT) (@cons iT l (@app iT ls (@nil iT))) (@cons iT l X)) with | eq_refl => @eq_refl (list iT) (@cons iT l (@app iT ls (@nil iT))) end in (eq _ t) return (hlist t) with | eq_refl => @Hcons l ls f h end *)
    rewrite IHh at 1.
(* Goal: @eq (hlist (@cons iT a (@app iT (@app iT ls ls') ls''))) (@Hcons a (@app iT (@app iT ls ls') ls'') (@hlist_hd a ls a0) match @eq_sym (list iT) (@app iT (@app iT ls ls') ls'') (@app iT ls (@app iT ls' ls'')) (@app_ass_trans iT ls ls' ls'') in (eq _ t) return (hlist t) with | eq_refl => @hlist_app ls (@app iT ls' ls'') (@hlist_tl a ls a0) (@hlist_app ls' ls'' b c) end) match @eq_sym (list iT) (@cons iT a (@app iT (@app iT ls ls') ls'')) (@cons iT a (@app iT ls (@app iT ls' ls''))) match @app_ass_trans iT ls ls' ls'' in (eq _ y) return (@eq (list iT) (@cons iT a (@app iT (@app iT ls ls') ls'')) (@cons iT a y)) with | eq_refl => @eq_refl (list iT) (@cons iT a (@app iT (@app iT ls ls') ls'')) end in (eq _ t) return (hlist t) with | eq_refl => @Hcons a (@app iT ls (@app iT ls' ls'')) (@hlist_hd a ls a0) (@hlist_app ls (@app iT ls' ls'') (@hlist_tl a ls a0) (@hlist_app ls' ls'' b c)) end *)
    unfold eq_trans. unfold f_equal. unfold eq_sym.
(* Goal: forall (T : Type@{Var(0)}) (U F : forall _ : T, Type@{Var(0)}) (R : forall (t : T) (_ : F t) (_ : F t), Prop) (R' : forall (t : T) (_ : U t) (_ : U t), Prop) (f g : forall (t : T) (_ : F t), U t) (_ : forall (t : T) (x y : F t) (_ : R t x y), R' t (f t x) (g t y)) (ls : list T) (a b : @hlist T F ls) (_ : @equiv_hlist T F R ls a b), @equiv_hlist T U R' ls (@hlist_map T F U f ls a) (@hlist_map T F U g ls b) *)
    clear. revert h.
(* Goal: forall h : hlist ls, @eq (hlist (@cons iT l (@app iT ls (@nil iT)))) (@Hcons l (@app iT ls (@nil iT)) f match match @app_nil_r_trans iT ls in (eq _ y) return (@eq (list iT) y (@app iT ls (@nil iT))) with | eq_refl => @eq_refl (list iT) (@app iT ls (@nil iT)) end in (eq _ t) return (hlist t) with | eq_refl => h end) match match match @app_nil_r_trans iT ls in (eq _ X) return (@eq (list iT) (@cons iT l (@app iT ls (@nil iT))) (@cons iT l X)) with | eq_refl => @eq_refl (list iT) (@cons iT l (@app iT ls (@nil iT))) end in (eq _ y) return (@eq (list iT) y (@cons iT l (@app iT ls (@nil iT)))) with | eq_refl => @eq_refl (list iT) (@cons iT l (@app iT ls (@nil iT))) end in (eq _ t) return (hlist t) with | eq_refl => @Hcons l ls f h end *)
    generalize dependent (app_nil_r_trans ls).
(* Goal: @eq (G t) (@hlist_hd A G t ls (@hlist_map A F G ff (@cons A t ls) (@Hcons A F t ls (@hlist_hd A F t ls hl) (@hlist_tl A F t ls hl)))) (@ff t (@hlist_hd A F t ls (@Hcons A F t ls (@hlist_hd A F t ls hl) (@hlist_tl A F t ls hl)))) *)
    destruct e. reflexivity.
  Qed.

  Fixpoint hlist_rev' ls ls' (h : hlist ls) : hlist ls' -> hlist (rev ls ++ ls') :=
    match h in hlist ls return hlist ls' -> hlist (rev ls ++ ls') with
    | Hnil => fun h => h
    | Hcons l ls0 x h' => fun hacc =>
      match app_ass_trans (rev ls0) (l :: nil) ls' in _ = t
            return hlist t -> hlist _
      with
      | eq_refl => fun x => x
      end (@hlist_rev' _ (l :: ls') h' (Hcons x hacc))
    end.

  Definition hlist_rev ls (h : hlist ls) : hlist (rev ls) :=
    match app_nil_r_trans (rev ls) in _ = t return hlist t with
      | eq_refl => hlist_rev' h Hnil
    end.

  Lemma hlist_rev_nil : hlist_rev Hnil = Hnil.
  Proof.
(* Goal: @eq (G t) (@hlist_hd A G t ls (@hlist_map A F G ff (@cons A t ls) (@Hcons A F t ls (@hlist_hd A F t ls hl) (@hlist_tl A F t ls hl)))) (@ff t (@hlist_hd A F t ls (@Hcons A F t ls (@hlist_hd A F t ls hl) (@hlist_tl A F t ls hl)))) *)
    reflexivity.
  Qed.

  (** TODO: I need hlist_rev_cons **)

  (** Equivalence **)
  (** TODO: This should change to relations **)
  Section equiv.
    Variable eqv : forall x, relation (F x).

    Inductive equiv_hlist : forall ls, hlist ls -> hlist ls -> Prop :=
    | hlist_eqv_nil : equiv_hlist Hnil Hnil
    | hlist_eqv_cons : forall l ls x y h1 h2, eqv x y -> equiv_hlist h1 h2 ->
      @equiv_hlist (l :: ls) (Hcons x h1) (Hcons y h2).

    Global Instance Reflexive_equiv_hlist (R : forall t, Reflexive (@eqv t)) ls
    : Reflexive (@equiv_hlist ls).
    Proof.
(* Goal: @eq (G t) (@hlist_hd A G t ls (@hlist_map A F G ff (@cons A t ls) (@Hcons A F t ls (@hlist_hd A F t ls hl) (@hlist_tl A F t ls hl)))) (@ff t (@hlist_hd A F t ls (@Hcons A F t ls (@hlist_hd A F t ls hl) (@hlist_tl A F t ls hl)))) *)
      red. induction x; constructor; auto. reflexivity.
    Qed.

    Global Instance Symmetric_equiv_hlist (R : forall t, Symmetric (@eqv t)) ls
    : Symmetric (@equiv_hlist ls).
    Proof.
(* Goal: @Symmetric (hlist ls) (@equiv_hlist ls) *)
      red. induction 1.
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
      { constructor. }
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
      { constructor. symmetry. assumption. auto. }
    Qed.

    Global Instance Transitive_equiv_hlist (R : forall t, Transitive (@eqv t)) ls
    : Transitive (@equiv_hlist ls).
    Proof.
(* Goal: @Symmetric (hlist ls) (@equiv_hlist ls) *)
      red. induction 1.
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
      { intro; assumption. }
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
      { rewrite (hlist_eta z).
        refine
          (fun H' =>
             match H' in @equiv_hlist ls X Y
                   return
                   match ls as ls return hlist ls -> hlist ls -> Prop with
                     | nil => fun _ _ : hlist nil => True
                     | l :: ls => fun (X Y : hlist (l :: ls)) =>
                                    forall Z x xs,
                                      eqv (hlist_hd Z) (hlist_hd X) ->
                                      equiv_hlist xs (hlist_tl X) ->
                                      (forall z : hlist ls,
                                         equiv_hlist (hlist_tl X) z ->
                                         equiv_hlist (hlist_tl Z) z) ->
                                      @equiv_hlist (l :: ls) Z Y
                   end X Y
             with
               | hlist_eqv_nil => I
               | hlist_eqv_cons l ls x y h1 h2 pf pf' => _
             end (Hcons x h1) x _ H H0 (@IHequiv_hlist)).
(* Goal: forall _ : @hlist_hrel A F G R (@app A (@cons A l ls0) ls) (@hlist_app A F (@cons A l ls0) ls (@Hcons A F l ls0 f x) xs) (@hlist_app A G (@cons A l ls0) ls (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y)) ys), and (@hlist_hrel A F G R (@cons A l ls0) (@Hcons A F l ls0 f x) (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y))) (@hlist_hrel A F G R ls xs ys) *)
        intros. rewrite (hlist_eta Z).
(* Goal: @hlist_hrel A F G R (@nil A) (@Hnil A F) (@Hnil A G) *)
        constructor. simpl in *. etransitivity. eassumption. eassumption.
        eapply H3. simpl in *. eassumption. }
    Qed.

    Lemma equiv_hlist_Hcons
    : forall ls i a b (c : hlist ls) d,
        equiv_hlist (Hcons a c) (@Hcons i ls b d) ->
        (@eqv i a b /\ equiv_hlist c d).
    Proof.
(* Goal: forall _ : @hlist_hrel A F G R (@app A (@cons A l ls0) ls) (@hlist_app A F (@cons A l ls0) ls (@Hcons A F l ls0 f x) xs) (@hlist_app A G (@cons A l ls0) ls (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y)) ys), and (@hlist_hrel A F G R (@cons A l ls0) (@Hcons A F l ls0 f x) (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y))) (@hlist_hrel A F G R ls xs ys) *)
      clear. intros.
      refine
        match H in @equiv_hlist ls' l r
              return match ls' as ls' return hlist ls' -> hlist ls' -> _ with
                       | nil => fun _ _ => True
                       | l :: ls => fun l r =>
                                      eqv (hlist_hd l) (hlist_hd r) /\
                                      equiv_hlist (hlist_tl l) (hlist_tl r)
                     end l r
        with
          | hlist_eqv_nil => I
          | hlist_eqv_cons _ _ _ _ _ _ pf pf' => conj pf pf'
        end.
    Defined.

    Lemma equiv_hlist_app
    : forall a b (c c' : hlist a)  (d d' : hlist b),
        (equiv_hlist c c' /\ equiv_hlist d d')
        <->
        equiv_hlist (hlist_app c d) (hlist_app c' d').
    Proof.
(* Goal: forall (T : Type@{Var(0)}) (U F : forall _ : T, Type@{Var(0)}) (R : forall (t : T) (_ : F t) (_ : F t), Prop) (R' : forall (t : T) (_ : U t) (_ : U t), Prop) (f g : forall (t : T) (_ : F t), U t) (_ : forall (t : T) (x y : F t) (_ : R t x y), R' t (f t x) (g t y)) (ls : list T) (a b : @hlist T F ls) (_ : @equiv_hlist T F R ls a b), @equiv_hlist T U R' ls (@hlist_map T F U f ls a) (@hlist_map T F U g ls b) *)
      clear. split.
      - destruct 1.
(* Goal: @equiv_hlist (@app iT a b) (@hlist_app a b c d) (@hlist_app a b c' d') *)
        induction H.
(* Goal: @eq (@hlist A G' ls) (@hlist_map A G G' gg ls (@hlist_map A F G ff ls hl)) (@hlist_map A (fun H : A => F H) (fun H : A => G' H) (fun (x : A) (x0 : F x) => @gg x (@ff x x0)) ls hl) *)
        + assumption.
(* Goal: forall t : A, R t (x t) (y t) *)
        + simpl. constructor; auto.
      - induction c.
        + rewrite (hlist_eta c').
(* Goal: @hlist_hrel A F G R (@nil A) (@Hnil A F) (@Hnil A G) *)
          simpl; intros; split; auto. constructor.
        + rewrite (hlist_eta c'); simpl.
(* Goal: forall _ : @equiv_hlist (@cons iT l (@app iT ls b)) (@Hcons l (@app iT ls b) f (@hlist_app ls b c d)) (@Hcons l (@app iT ls b) (@hlist_hd l ls c') (@hlist_app ls b (@hlist_tl l ls c') d')), and (@equiv_hlist (@cons iT l ls) (@Hcons l ls f c) (@Hcons l ls (@hlist_hd l ls c') (@hlist_tl l ls c'))) (@equiv_hlist b d d') *)
          specialize (IHc (hlist_tl c')).
(* Goal: forall e : @eq (list iT) (@app iT ls (@app iT ls' ls'')) (@app iT ls (@app iT ls' ls'')), @eq (hlist (@cons iT a (@app iT ls (@app iT ls' ls'')))) (@Hcons a (@app iT ls (@app iT ls' ls'')) (@hlist_hd a ls a0) match match e in (eq _ y) return (@eq (list iT) y (@app iT ls (@app iT ls' ls''))) with | eq_refl => @eq_refl (list iT) (@app iT ls (@app iT ls' ls'')) end in (eq _ t) return (hlist t) with | eq_refl => @hlist_app ls (@app iT ls' ls'') (@hlist_tl a ls a0) (@hlist_app ls' ls'' b c) end) match match match e in (eq _ y) return (@eq (list iT) (@cons iT a (@app iT ls (@app iT ls' ls''))) (@cons iT a y)) with | eq_refl => @eq_refl (list iT) (@cons iT a (@app iT ls (@app iT ls' ls''))) end in (eq _ y) return (@eq (list iT) y (@cons iT a (@app iT ls (@app iT ls' ls'')))) with | eq_refl => @eq_refl (list iT) (@cons iT a (@app iT ls (@app iT ls' ls''))) end in (eq _ t) return (hlist t) with | eq_refl => @Hcons a (@app iT ls (@app iT ls' ls'')) (@hlist_hd a ls a0) (@hlist_app ls (@app iT ls' ls'') (@hlist_tl a ls a0) (@hlist_app ls' ls'' b c)) end *)
          intro.
(* Goal: and (@equiv_hlist (@cons iT l ls) (@Hcons l ls f c) (@Hcons l ls (@hlist_hd l ls c') (@hlist_tl l ls c'))) (@equiv_hlist b d d') *)
          eapply equiv_hlist_Hcons in H. intuition.
(* Goal: forall t : A, R t (x t) (y t) *)
          constructor; auto.
    Qed.

    Global Instance Injection_equiv_hlist_cons ls i a b (c : hlist ls) d
    : Injective (equiv_hlist (Hcons a c) (@Hcons i ls b d)) :=
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
    { result := @eqv i a b /\ equiv_hlist c d
    ; injection := @equiv_hlist_Hcons _ _ _ _ _ _ }.

    Global Instance Injection_equiv_hlist_app a b (c c' : hlist a) (d d' : hlist b)
    : Injective (equiv_hlist (hlist_app c d) (hlist_app c' d')) :=
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
    { result := equiv_hlist c c' /\ equiv_hlist d d'
    ; injection := fun x => proj2 (@equiv_hlist_app _ _ _ _ _ _) x }.

  End equiv.

  Lemma hlist_nil_eta : forall (h : hlist nil), h = Hnil.
  Proof.
(* Goal: @eq (G t) (@hlist_hd A G t ls (@hlist_map A F G ff (@cons A t ls) (@Hcons A F t ls (@hlist_hd A F t ls hl) (@hlist_tl A F t ls hl)))) (@ff t (@hlist_hd A F t ls (@Hcons A F t ls (@hlist_hd A F t ls hl) (@hlist_tl A F t ls hl)))) *)
    intros; rewrite (hlist_eta h); reflexivity.
  Qed.

  Lemma hlist_cons_eta : forall a b (h : hlist (a :: b)),
    h = Hcons (hlist_hd h) (hlist_tl h).
  Proof.
(* Goal: @eq (G t) (@hlist_hd A G t ls (@hlist_map A F G ff (@cons A t ls) (@Hcons A F t ls (@hlist_hd A F t ls hl) (@hlist_tl A F t ls hl)))) (@ff t (@hlist_hd A F t ls (@Hcons A F t ls (@hlist_hd A F t ls hl) (@hlist_tl A F t ls hl)))) *)
    intros; rewrite (hlist_eta h); reflexivity.
  Qed.

  Lemma Hcons_inv
  : forall l ls a b c d,
      @eq (hlist (l :: ls)) (Hcons a b) (Hcons c d) ->
      a = c /\ b = d.
  Proof.
(* Goal: forall _ : @hlist_hrel A F G R (@app A (@cons A l ls0) ls) (@hlist_app A F (@cons A l ls0) ls (@Hcons A F l ls0 f x) xs) (@hlist_app A G (@cons A l ls0) ls (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y)) ys), and (@hlist_hrel A F G R (@cons A l ls0) (@Hcons A F l ls0 f x) (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y))) (@hlist_hrel A F G R ls xs ys) *)
    intros.
    refine (
        match H as K in _ = Z
              return match Z in hlist LS
                           return match LS with
                                    | nil => Prop
                                    | l :: ls => F l -> hlist ls -> Prop
                                  end
                     with
                       | Hcons X Y x y => fun a b => a = x /\ b = y
                       | Hnil => True
                     end a b
        with
          | eq_refl => conj eq_refl eq_refl
        end).
  Qed.

  Global Instance Injection_hlist_cons ls t (a : F t) (b : hlist ls) c d
  : Injective (Hcons a b = Hcons c d) :=
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
    { result := a = c /\ b = d
    ; injection := @Hcons_inv t ls a b c d
    }.


  Theorem equiv_eq_eq : forall ls (x y : hlist ls),
                          equiv_hlist (fun x => @eq _) x y <-> x = y.
  Proof.
(* Goal: forall _ : @hlist_hrel A F G R (@app A (@cons A l ls0) ls) (@hlist_app A F (@cons A l ls0) ls (@Hcons A F l ls0 f x) xs) (@hlist_app A G (@cons A l ls0) ls (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y)) ys), and (@hlist_hrel A F G R (@cons A l ls0) (@Hcons A F l ls0 f x) (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y))) (@hlist_hrel A F G R ls xs ys) *)
    induction x; simpl; intros.
(* Goal: @eq (G t) (@hlist_hd A G t ls (@hlist_map A F G ff (@cons A t ls) (@Hcons A F t ls (@hlist_hd A F t ls hl) (@hlist_tl A F t ls hl)))) (@ff t (@hlist_hd A F t ls (@Hcons A F t ls (@hlist_hd A F t ls hl) (@hlist_tl A F t ls hl)))) *)
    { split. inversion 1. rewrite hlist_nil_eta. reflexivity.
(* Goal: @hlist_hrel A F G R (@nil A) (@Hnil A F) (@Hnil A G) *)
      intros; subst; constructor. }
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
    { split.
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
      { intro. rewrite (hlist_eta y).
(* Goal: @eq (hlist (@cons iT l ls)) (@Hcons l ls f x) (@Hcons l ls (@hlist_hd l ls y) (@hlist_tl l ls y)) *)
        specialize (IHx (hlist_tl y)).
        refine (match H in @equiv_hlist _ LS X Y
                      return match X in hlist LS
                                   return F match LS with
                                              | nil => l
                                              | l :: _ => l
                                            end ->
                                          hlist match LS with
                                                  | nil => ls
                                                  | _ :: ls => ls
                                                end ->
                                          Prop
                             with
                               | Hnil => fun _ _ => True
                               | Hcons a b c d => fun x y =>
                                                    (equiv_hlist (fun x0 : iT => eq) d y <-> d = y) ->
                                                    @Hcons a b c d = Hcons x y
                             end (match LS as LS return hlist LS -> F match LS with
                                                                        | nil => l
                                                                        | l :: _ => l
                                                                      end
                                  with
                                    | nil => fun _ => f
                                    | l :: ls => hlist_hd
                                  end Y)
                                 (match LS as LS return hlist LS -> hlist match LS with
                                                                            | nil => ls
                                                                            | _ :: ls => ls
                                                                          end
                                  with
                                    | nil => fun _ => x
                                    | l :: ls => hlist_tl
                                  end Y)
                with
                  | hlist_eqv_nil => I
                  | hlist_eqv_cons l ls x y h1 h2 pf1 pf2 => _
                end IHx).
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) (@Hcons A F l ls (@hlist_hd A F l ls hl) (@hlist_tl A F l ls hl))))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls (@Hcons A F l ls (@hlist_hd A F l ls hl) (@hlist_tl A F l ls hl))))) *)
        simpl.
(* Goal: forall _ : @hlist_hrel A F G R (@app A (@cons A l ls0) ls) (@hlist_app A F (@cons A l ls0) ls (@Hcons A F l ls0 f x) xs) (@hlist_app A G (@cons A l ls0) ls (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y)) ys), and (@hlist_hrel A F G R (@cons A l ls0) (@Hcons A F l ls0 f x) (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y))) (@hlist_hrel A F G R ls xs ys) *)
        subst. intros.
        f_equal. apply H0. assumption. }
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
      { intros; subst. constructor; auto.
(* Goal: @eq (G t) (@hlist_hd A G t ls (@hlist_map A F G ff (@cons A t ls) (@Hcons A F t ls (@hlist_hd A F t ls hl) (@hlist_tl A F t ls hl)))) (@ff t (@hlist_hd A F t ls (@Hcons A F t ls (@hlist_hd A F t ls hl) (@hlist_tl A F t ls hl)))) *)
        reflexivity. } }
  Qed.

  Fixpoint hlist_get ls a (m : member a ls) : hlist ls -> F a :=
    match m in member _ ls return hlist ls -> F a with
      | MZ _ => hlist_hd
      | MN _ _ r => fun hl => hlist_get r (hlist_tl hl)
    end.

(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
  Fixpoint hlist_nth_error {ls} (hs : hlist ls) (n : nat)
    : option (match nth_error ls n with
                | None => unit
                | Some x => F x
              end) :=
    match hs in hlist ls return option (match nth_error ls n with
                                          | None => unit
                                          | Some x => F x
                                        end)
      with
      | Hnil => None
      | Hcons l ls h hs =>
        match n as n return option (match nth_error (l :: ls) n with
                                      | None => unit
                                      | Some x => F x
                                    end)
          with
          | 0 => Some h
          | S n => hlist_nth_error hs n
        end
    end.

  Polymorphic Fixpoint hlist_nth ls (h : hlist ls) (n : nat) :
    match nth_error ls n return Type with
      | None => unit
      | Some t => F t
    end :=
    match h in hlist ls , n as n
      return match nth_error ls n with
               | None => unit
               | Some t => F t
             end
      with
      | Hnil , 0 => tt
      | Hnil , S _ => tt
      | Hcons _ _ x _ , 0 => x
      | Hcons _ _ _ h , S n => hlist_nth h n
    end.

  Fixpoint nth_error_hlist_nth ls (n : nat)
  : option (hlist ls -> match nth_error ls n with
                          | None => Empty_set
                          | Some x => F x
                        end) :=
    match ls as ls
          return option (hlist ls -> match nth_error ls n with
                                       | None => Empty_set
                                       | Some x => F x
                                     end)
    with
      | nil => None
      | l :: ls =>
        match n as n
              return option (hlist (l :: ls) -> match nth_error (l :: ls) n with
                                                  | None => Empty_set
                                                  | Some x => F x
                                                end)
        with
          | 0 => Some hlist_hd
          | S n =>
            match nth_error_hlist_nth ls n with
              | None => None
              | Some f => Some (fun h => f (hlist_tl h))
            end
        end
    end.

  Definition cast1 T l
  : forall (l' : list T) n v,
      nth_error l n = Some v -> Some v = nth_error (l ++ l') n.
  Proof.
(* Goal: forall _ : @hlist_hrel A F G R (@app A (@cons A l ls0) ls) (@hlist_app A F (@cons A l ls0) ls (@Hcons A F l ls0 f x) xs) (@hlist_app A G (@cons A l ls0) ls (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y)) ys), and (@hlist_hrel A F G R (@cons A l ls0) (@Hcons A F l ls0 f x) (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y))) (@hlist_hrel A F G R ls xs ys) *)
    induction l. intros.
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
    { exfalso. destruct n; inversion H. }
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
    { destruct n; simpl; intros; auto. }
  Defined.

  Definition cast2 T l
  : forall (l' : list T) n,
      nth_error l n = None ->
      nth_error l' (n - length l) = nth_error (l ++ l') n.
  Proof.
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) (@Hcons A F l ls (@hlist_hd A F l ls hl) (@hlist_tl A F l ls hl))))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls (@Hcons A F l ls (@hlist_hd A F l ls hl) (@hlist_tl A F l ls hl))))) *)
    induction l; simpl.
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
    { destruct n; simpl; auto. }
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
    { destruct n; simpl; auto.
      inversion 1. }
  Defined.

  Theorem hlist_nth_hlist_app
  : forall l l' (h : hlist l) (h' : hlist l') n,
    hlist_nth (hlist_app h h') n =
    match nth_error l n as k
      return nth_error l n = k ->
      match nth_error (l ++ l') n return Type with
        | None => unit
        | Some t => F t
      end
    with
      | Some _ => fun pf =>
        match
          cast1 _ _ _ pf in _ = z ,
          eq_sym pf in _ = w
          return match w return Type with
                   | None => unit
                   | Some t => F t
                 end ->
                 match z return Type with
                   | None => unit
                   | Some t => F t
                 end
        with
          | eq_refl , eq_refl => fun x => x
        end (hlist_nth h n)
      | None => fun pf =>
        match cast2 _ _ _ pf in _ = z
          return match z with
                   | Some t => F t
                   | None => unit
                 end
        with
          | eq_refl => hlist_nth h' (n - length l)
        end
    end eq_refl.
  Proof.
(* Goal: forall _ : @hlist_hrel A F G R (@app A (@cons A l ls0) ls) (@hlist_app A F (@cons A l ls0) ls (@Hcons A F l ls0 f x) xs) (@hlist_app A G (@cons A l ls0) ls (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y)) ys), and (@hlist_hrel A F G R (@cons A l ls0) (@Hcons A F l ls0 f x) (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y))) (@hlist_hrel A F G R ls xs ys) *)
    induction h; simpl; intros.
(* Goal: @eq (G t) (@hlist_hd A G t ls (@hlist_map A F G ff (@cons A t ls) (@Hcons A F t ls (@hlist_hd A F t ls hl) (@hlist_tl A F t ls hl)))) (@ff t (@hlist_hd A F t ls (@Hcons A F t ls (@hlist_hd A F t ls hl) (@hlist_tl A F t ls hl)))) *)
    { destruct n; simpl in *; reflexivity. }
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
    { destruct n; simpl.
(* Goal: @eq (G t) (@hlist_hd A G t ls (@hlist_map A F G ff (@cons A t ls) (@Hcons A F t ls (@hlist_hd A F t ls hl) (@hlist_tl A F t ls hl)))) (@ff t (@hlist_hd A F t ls (@Hcons A F t ls (@hlist_hd A F t ls hl) (@hlist_tl A F t ls hl)))) *)
      { reflexivity. }
(* Goal: @eq (G t) (@hlist_hd A G t ls (@hlist_map A F G ff (@cons A t ls) (@Hcons A F t ls (@hlist_hd A F t ls hl) (@hlist_tl A F t ls hl)))) (@ff t (@hlist_hd A F t ls (@Hcons A F t ls (@hlist_hd A F t ls hl) (@hlist_tl A F t ls hl)))) *)
      { rewrite IHh. reflexivity. } }
  Qed.

  Section type.
    Variable eqv : forall x, type (F x).

    Global Instance type_hlist (ls : list iT): type (hlist ls) :=
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
    { equal := @equiv_hlist (fun x => @equal _ (eqv x)) ls
    ; proper :=
      (fix recur ls (h : hlist ls) : Prop :=
        match h with
          | Hnil => True
          | Hcons _ _ x y => proper x /\ recur _ y
        end) ls
    }.

    Variable eqvOk : forall x, typeOk (eqv x).

    Global Instance typeOk_hlist (ls : list iT): typeOk (type_hlist ls).
    Proof.
(* Goal: @hlist_hrel A F G R (@nil A) (@Hnil A F) (@Hnil A G) *)
      constructor.
(* Goal: forall _ : @hlist_hrel A F G R (@app A (@cons A l ls0) ls) (@hlist_app A F (@cons A l ls0) ls (@Hcons A F l ls0 f x) xs) (@hlist_app A G (@cons A l ls0) ls (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y)) ys), and (@hlist_hrel A F G R (@cons A l ls0) (@Hcons A F l ls0 f x) (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y))) (@hlist_hrel A F G R ls xs ys) *)
      { induction ls; intros.
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
        { rewrite (hlist_eta x) in *. rewrite (hlist_eta y) in *.
(* Goal: forall (T : Type@{Var(0)}) (U F : forall _ : T, Type@{Var(0)}) (R : forall (t : T) (_ : F t) (_ : F t), Prop) (R' : forall (t : T) (_ : U t) (_ : U t), Prop) (f g : forall (t : T) (_ : F t), U t) (_ : forall (t : T) (x y : F t) (_ : R t x y), R' t (f t x) (g t y)) (ls : list T) (a b : @hlist T F ls) (_ : @equiv_hlist T F R ls a b), @equiv_hlist T U R' ls (@hlist_map T F U f ls a) (@hlist_map T F U g ls b) *)
          clear. compute; auto. }
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
        { rewrite (hlist_eta x) in *. rewrite (hlist_eta y) in *.
          simpl in H.
          inv_all. eapply IHls in H1.
(* Goal: forall t : A, R t (x t) (y t) *)
          eapply only_proper in H0; eauto.
          simpl; tauto. } }
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
      { intro. induction ls; simpl.
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
        { rewrite (hlist_eta x); intros; constructor. }
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
        { rewrite (hlist_eta x); intros; intuition; constructor.
          eapply preflexive; [ | eauto with typeclass_instances ].
          eauto with typeclass_instances.
          eapply IHls; eauto. } }
(* Goal: @Symmetric (hlist ls) (@equiv_hlist ls) *)
      { red. induction 1.
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
        { constructor. }
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
        { constructor. symmetry. assumption. assumption. } }
(* Goal: @Symmetric (hlist ls) (@equiv_hlist ls) *)
      { red. induction 1.
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
        { auto. }
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
        { intro H1.
          etransitivity; [ | eassumption ].
          constructor; eauto. } }
    Qed.

    Global Instance proper_hlist_app l l' : proper (@hlist_app l l').
    Proof.
(* Goal: @Symmetric (hlist ls) (@equiv_hlist ls) *)
      do 6 red. induction 1; simpl; auto.
(* Goal: forall _ : @hlist_hrel A F G R (@app A (@cons A l ls0) ls) (@hlist_app A F (@cons A l ls0) ls (@Hcons A F l ls0 f x) xs) (@hlist_app A G (@cons A l ls0) ls (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y)) ys), and (@hlist_hrel A F G R (@cons A l ls0) (@Hcons A F l ls0 f x) (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y))) (@hlist_hrel A F G R ls xs ys) *)
      { intros. constructor; eauto.
        eapply IHequiv_hlist. exact H1. }
    Qed.

    Lemma hlist_app_assoc : forall ls ls' ls''
                                 (a : hlist ls) (b : hlist ls') (c : hlist ls''),
      hlist_app (hlist_app a b) c =
      match eq_sym (app_ass_trans ls ls' ls'') in _ = t return hlist t with
        | eq_refl => hlist_app a (hlist_app b c)
      end.
    Proof.
(* Goal: forall (ls ls' ls'' : list iT) (a : hlist ls) (b : hlist ls') (c : hlist ls''), @eq (hlist (@app iT (@app iT ls ls') ls'')) (@hlist_app (@app iT ls ls') ls'' (@hlist_app ls ls' a b) c) match @eq_sym (list iT) (@app iT (@app iT ls ls') ls'') (@app iT ls (@app iT ls' ls'')) (@app_ass_trans iT ls ls' ls'') in (eq _ t) return (hlist t) with | eq_refl => @hlist_app ls (@app iT ls' ls'') a (@hlist_app ls' ls'' b c) end *)
      intros ls ls' ls''.
(* Goal: forall (a : hlist ls) (b : hlist ls') (c : hlist ls''), @eq (hlist (@app iT (@app iT ls ls') ls'')) (@hlist_app (@app iT ls ls') ls'' (@hlist_app ls ls' a b) c) match @eq_sym (list iT) (@app iT (@app iT ls ls') ls'') (@app iT ls (@app iT ls' ls'')) (@app_ass_trans iT ls ls' ls'') in (eq _ t) return (hlist t) with | eq_refl => @hlist_app ls (@app iT ls' ls'') a (@hlist_app ls' ls'' b c) end *)
      generalize (eq_sym (app_assoc_reverse ls ls' ls'')).
(* Goal: forall _ : @hlist_hrel A F G R (@app A (@cons A l ls0) ls) (@hlist_app A F (@cons A l ls0) ls (@Hcons A F l ls0 f x) xs) (@hlist_app A G (@cons A l ls0) ls (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y)) ys), and (@hlist_hrel A F G R (@cons A l ls0) (@Hcons A F l ls0 f x) (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y))) (@hlist_hrel A F G R ls xs ys) *)
      induction ls; simpl; intros.
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
      { rewrite (hlist_eta a); simpl.
(* Goal: @eq (G t) (@hlist_hd A G t ls (@hlist_map A F G ff (@cons A t ls) (@Hcons A F t ls (@hlist_hd A F t ls hl) (@hlist_tl A F t ls hl)))) (@ff t (@hlist_hd A F t ls (@Hcons A F t ls (@hlist_hd A F t ls hl) (@hlist_tl A F t ls hl)))) *)
        reflexivity. }
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
      { rewrite (hlist_eta a0). simpl.
(* Goal: @ex (forall _ : hlist tvs', F (@projT1 iT (fun t : iT => forall _ : hlist (@cons iT a (@app iT tvs tvs')), F t) x)) (fun y : forall _ : hlist tvs', F (@projT1 iT (fun t : iT => forall _ : hlist (@cons iT a (@app iT tvs tvs')), F t) x) => and (@eq (option (@sigT iT (fun t : iT => forall _ : hlist tvs', F t))) (nth_error_get_hlist_nth tvs' (Nat.sub O (S (@length iT tvs)))) (@Some (@sigT iT (fun t : iT => forall _ : hlist tvs', F t)) (@existT iT (fun t : iT => forall _ : hlist tvs', F t) (@projT1 iT (fun t : iT => forall _ : hlist (@cons iT a (@app iT tvs tvs')), F t) x) y))) (forall (vs : hlist (@cons iT a tvs)) (vs' : hlist tvs'), @eq (F (@projT1 iT (fun t : iT => forall _ : hlist (@cons iT a (@app iT tvs tvs')), F t) x)) (@projT2 iT (fun t : iT => forall _ : hlist (@cons iT a (@app iT tvs tvs')), F t) x (@hlist_app (@cons iT a tvs) tvs' vs vs')) (y vs'))) *)
        inversion H.
(* Goal: @eq (hlist (@cons iT a (@app iT (@app iT ls ls') ls''))) (@Hcons a (@app iT (@app iT ls ls') ls'') (@hlist_hd a ls a0) (@hlist_app (@app iT ls ls') ls'' (@hlist_app ls ls' (@hlist_tl a ls a0) b) c)) match @eq_sym (list iT) (@cons iT a (@app iT (@app iT ls ls') ls'')) (@cons iT a (@app iT ls (@app iT ls' ls''))) match @app_ass_trans iT ls ls' ls'' in (eq _ y) return (@eq (list iT) (@cons iT a (@app iT (@app iT ls ls') ls'')) (@cons iT a y)) with | eq_refl => @eq_refl (list iT) (@cons iT a (@app iT (@app iT ls ls') ls'')) end in (eq _ t) return (hlist t) with | eq_refl => @Hcons a (@app iT ls (@app iT ls' ls'')) (@hlist_hd a ls a0) (@hlist_app ls (@app iT ls' ls'') (@hlist_tl a ls a0) (@hlist_app ls' ls'' b c)) end *)
        erewrite (IHls H1).
(* Goal: @eq (hlist (@cons iT a (@app iT (@app iT ls ls') ls''))) (@Hcons a (@app iT (@app iT ls ls') ls'') (@hlist_hd a ls a0) match @eq_sym (list iT) (@app iT (@app iT ls ls') ls'') (@app iT ls (@app iT ls' ls'')) (@app_ass_trans iT ls ls' ls'') in (eq _ t) return (hlist t) with | eq_refl => @hlist_app ls (@app iT ls' ls'') (@hlist_tl a ls a0) (@hlist_app ls' ls'' b c) end) match @eq_sym (list iT) (@cons iT a (@app iT (@app iT ls ls') ls'')) (@cons iT a (@app iT ls (@app iT ls' ls''))) match @app_ass_trans iT ls ls' ls'' in (eq _ y) return (@eq (list iT) (@cons iT a (@app iT (@app iT ls ls') ls'')) (@cons iT a y)) with | eq_refl => @eq_refl (list iT) (@cons iT a (@app iT (@app iT ls ls') ls'')) end in (eq _ t) return (hlist t) with | eq_refl => @Hcons a (@app iT ls (@app iT ls' ls'')) (@hlist_hd a ls a0) (@hlist_app ls (@app iT ls' ls'') (@hlist_tl a ls a0) (@hlist_app ls' ls'' b c)) end *)
        unfold f_equal. unfold eq_trans. unfold eq_sym.
(* Goal: @eq (hlist (@cons iT a (@app iT (@app iT ls ls') ls''))) (@Hcons a (@app iT (@app iT ls ls') ls'') (@hlist_hd a ls a0) match match @app_ass_trans iT ls ls' ls'' in (eq _ y) return (@eq (list iT) y (@app iT (@app iT ls ls') ls'')) with | eq_refl => @eq_refl (list iT) (@app iT (@app iT ls ls') ls'') end in (eq _ t) return (hlist t) with | eq_refl => @hlist_app ls (@app iT ls' ls'') (@hlist_tl a ls a0) (@hlist_app ls' ls'' b c) end) match match match @app_ass_trans iT ls ls' ls'' in (eq _ y) return (@eq (list iT) (@cons iT a (@app iT (@app iT ls ls') ls'')) (@cons iT a y)) with | eq_refl => @eq_refl (list iT) (@cons iT a (@app iT (@app iT ls ls') ls'')) end in (eq _ y) return (@eq (list iT) y (@cons iT a (@app iT (@app iT ls ls') ls''))) with | eq_refl => @eq_refl (list iT) (@cons iT a (@app iT (@app iT ls ls') ls'')) end in (eq _ t) return (hlist t) with | eq_refl => @Hcons a (@app iT ls (@app iT ls' ls'')) (@hlist_hd a ls a0) (@hlist_app ls (@app iT ls' ls'') (@hlist_tl a ls a0) (@hlist_app ls' ls'' b c)) end *)
        generalize (app_ass_trans ls ls' ls'').
        rewrite <- H1.
(* Goal: forall (T : Type@{Var(0)}) (U F : forall _ : T, Type@{Var(0)}) (R : forall (t : T) (_ : F t) (_ : F t), Prop) (R' : forall (t : T) (_ : U t) (_ : U t), Prop) (f g : forall (t : T) (_ : F t), U t) (_ : forall (t : T) (x y : F t) (_ : R t x y), R' t (f t x) (g t y)) (ls : list T) (a b : @hlist T F ls) (_ : @equiv_hlist T F R ls a b), @equiv_hlist T U R' ls (@hlist_map T F U f ls a) (@hlist_map T F U g ls b) *)
        clear. intro.
(* Goal: @eq (hlist (@cons iT a (@app iT ls (@app iT ls' ls'')))) (@Hcons a (@app iT ls (@app iT ls' ls'')) (@hlist_hd a ls a0) match match e in (eq _ y) return (@eq (list iT) y (@app iT ls (@app iT ls' ls''))) with | eq_refl => @eq_refl (list iT) (@app iT ls (@app iT ls' ls'')) end in (eq _ t) return (hlist t) with | eq_refl => @hlist_app ls (@app iT ls' ls'') (@hlist_tl a ls a0) (@hlist_app ls' ls'' b c) end) match match match e in (eq _ y) return (@eq (list iT) (@cons iT a (@app iT ls (@app iT ls' ls''))) (@cons iT a y)) with | eq_refl => @eq_refl (list iT) (@cons iT a (@app iT ls (@app iT ls' ls''))) end in (eq _ y) return (@eq (list iT) y (@cons iT a (@app iT ls (@app iT ls' ls'')))) with | eq_refl => @eq_refl (list iT) (@cons iT a (@app iT ls (@app iT ls' ls''))) end in (eq _ t) return (hlist t) with | eq_refl => @Hcons a (@app iT ls (@app iT ls' ls'')) (@hlist_hd a ls a0) (@hlist_app ls (@app iT ls' ls'') (@hlist_tl a ls a0) (@hlist_app ls' ls'' b c)) end *)
        generalize dependent (hlist_app (hlist_tl a0) (hlist_app b c)).
(* Goal: @eq (G t) (@hlist_hd A G t ls (@hlist_map A F G ff (@cons A t ls) (@Hcons A F t ls (@hlist_hd A F t ls hl) (@hlist_tl A F t ls hl)))) (@ff t (@hlist_hd A F t ls (@Hcons A F t ls (@hlist_hd A F t ls hl) (@hlist_tl A F t ls hl)))) *)
        destruct e. reflexivity. }
    Qed.

    Lemma hlist_app_assoc'
      : forall (ls ls' ls'' : list iT)
               (a : hlist ls) (b : hlist ls') (c : hlist ls''),
        hlist_app a (hlist_app b c) =
        match
          app_ass_trans ls ls' ls'' in (_ = t) return (hlist t)
        with
        | eq_refl => hlist_app (hlist_app a b) c
        end.
    Proof.
(* Goal: forall _ : @hlist_hrel A F G R (@app A (@cons A l ls0) ls) (@hlist_app A F (@cons A l ls0) ls (@Hcons A F l ls0 f x) xs) (@hlist_app A G (@cons A l ls0) ls (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y)) ys), and (@hlist_hrel A F G R (@cons A l ls0) (@Hcons A F l ls0 f x) (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y))) (@hlist_hrel A F G R ls xs ys) *)
      clear. intros.
(* Goal: @eq (hlist (@app iT ls (@app iT ls' ls''))) (@hlist_app ls (@app iT ls' ls'') a (@hlist_app ls' ls'' b c)) match @app_ass_trans iT ls ls' ls'' in (eq _ t) return (hlist t) with | eq_refl => @hlist_app (@app iT ls ls') ls'' (@hlist_app ls ls' a b) c end *)
      generalize (hlist_app_assoc a b c).
(* Goal: forall _ : @eq (hlist (@app iT (@app iT ls ls') ls'')) (@hlist_app (@app iT ls ls') ls'' (@hlist_app ls ls' a b) c) match @eq_sym (list iT) (@app iT (@app iT ls ls') ls'') (@app iT ls (@app iT ls' ls'')) (@app_ass_trans iT ls ls' ls'') in (eq _ t) return (hlist t) with | eq_refl => @hlist_app ls (@app iT ls' ls'') a (@hlist_app ls' ls'' b c) end, @eq (hlist (@app iT ls (@app iT ls' ls''))) (@hlist_app ls (@app iT ls' ls'') a (@hlist_app ls' ls'' b c)) match @app_ass_trans iT ls ls' ls'' in (eq _ t) return (hlist t) with | eq_refl => @hlist_app (@app iT ls ls') ls'' (@hlist_app ls ls' a b) c end *)
      generalize (hlist_app (hlist_app a b) c).
(* Goal: forall (h : hlist (@app iT (@app iT ls ls') ls'')) (_ : @eq (hlist (@app iT (@app iT ls ls') ls'')) h match @eq_sym (list iT) (@app iT (@app iT ls ls') ls'') (@app iT ls (@app iT ls' ls'')) (@app_ass_trans iT ls ls' ls'') in (eq _ t) return (hlist t) with | eq_refl => @hlist_app ls (@app iT ls' ls'') a (@hlist_app ls' ls'' b c) end), @eq (hlist (@app iT ls (@app iT ls' ls''))) (@hlist_app ls (@app iT ls' ls'') a (@hlist_app ls' ls'' b c)) match @app_ass_trans iT ls ls' ls'' in (eq _ t) return (hlist t) with | eq_refl => h end *)
      generalize (hlist_app a (hlist_app b c)).
(* Goal: forall (h : hlist (@app iT ls (@app iT ls' ls''))) (h0 : hlist (@app iT (@app iT ls ls') ls'')) (_ : @eq (hlist (@app iT (@app iT ls ls') ls'')) h0 match @eq_sym (list iT) (@app iT (@app iT ls ls') ls'') (@app iT ls (@app iT ls' ls'')) (@app_ass_trans iT ls ls' ls'') in (eq _ t) return (hlist t) with | eq_refl => h end), @eq (hlist (@app iT ls (@app iT ls' ls''))) h match @app_ass_trans iT ls ls' ls'' in (eq _ t) return (hlist t) with | eq_refl => h0 end *)
      destruct (app_ass_trans ls ls' ls'').
(* Goal: forall t : A, R t (x t) (y t) *)
      simpl. auto.
    Qed.

    Fixpoint hlist_split ls ls' : hlist (ls ++ ls') -> hlist ls * hlist ls' :=
      match ls as ls return hlist (ls ++ ls') -> hlist ls * hlist ls' with
        | nil => fun h => (Hnil, h)
        | l :: ls => fun h =>
                       let (a,b) := @hlist_split ls ls' (hlist_tl h) in
                       (Hcons (hlist_hd h) a, b)
      end.

    Lemma hlist_app_hlist_split : forall ls' ls (h : hlist (ls ++ ls')),
      hlist_app (fst (hlist_split ls ls' h)) (snd (hlist_split ls ls' h)) = h.
    Proof.
(* Goal: forall t : A, R t (x t) (y t) *)
      induction ls; simpl; intros; auto.
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) (@Hcons A F l ls (@hlist_hd A F l ls hl) (@hlist_tl A F l ls hl))))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls (@Hcons A F l ls (@hlist_hd A F l ls hl) (@hlist_tl A F l ls hl))))) *)
      rewrite (hlist_eta h); simpl.
(* Goal: @eq (hlist (@cons iT a (@app iT ls ls'))) (@hlist_app (@cons iT a ls) ls' (@fst (hlist (@cons iT a ls)) (hlist ls') (let (a0, b) := hlist_split ls ls' (@hlist_tl a (@app iT ls ls') h) in @pair (hlist (@cons iT a ls)) (hlist ls') (@Hcons a ls (@hlist_hd a (@app iT ls ls') h) a0) b)) (@snd (hlist (@cons iT a ls)) (hlist ls') (let (a0, b) := hlist_split ls ls' (@hlist_tl a (@app iT ls ls') h) in @pair (hlist (@cons iT a ls)) (hlist ls') (@Hcons a ls (@hlist_hd a (@app iT ls ls') h) a0) b))) (@Hcons a (@app iT ls ls') (@hlist_hd a (@app iT ls ls') h) (@hlist_tl a (@app iT ls ls') h)) *)
      specialize (IHls (hlist_tl h)).
(* Goal: forall t : A, R t (x t) (y t) *)
      destruct (hlist_split ls ls' (hlist_tl h)); simpl in *; auto.
(* Goal: forall t : A, R t (x t) (y t) *)
      f_equal. auto.
    Qed.

    Lemma hlist_split_hlist_app : forall ls' ls (h : hlist ls) (h' : hlist ls'),
      hlist_split _ _ (hlist_app h h') = (h,h').
    Proof.
(* Goal: forall _ : @hlist_hrel A F G R (@app A (@cons A l ls0) ls) (@hlist_app A F (@cons A l ls0) ls (@Hcons A F l ls0 f x) xs) (@hlist_app A G (@cons A l ls0) ls (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y)) ys), and (@hlist_hrel A F G R (@cons A l ls0) (@Hcons A F l ls0 f x) (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y))) (@hlist_hrel A F G R ls xs ys) *)
      induction ls; simpl; intros.
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
      { rewrite (hlist_eta h); simpl; auto. }
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
      { rewrite (hlist_eta h); simpl.
(* Goal: @eq (G t) (@hlist_hd A G t ls (@hlist_map A F G ff (@cons A t ls) (@Hcons A F t ls (@hlist_hd A F t ls hl) (@hlist_tl A F t ls hl)))) (@ff t (@hlist_hd A F t ls (@Hcons A F t ls (@hlist_hd A F t ls hl) (@hlist_tl A F t ls hl)))) *)
        rewrite IHls. reflexivity. }
    Qed.

  End type.

  Lemma hlist_hd_fst_hlist_split
  : forall t (xs ys : list _) (h : hlist (t :: xs ++ ys)),
      hlist_hd (fst (hlist_split (t :: xs) ys h)) = hlist_hd h.
  Proof.
(* Goal: forall _ : @hlist_hrel A F G R (@app A (@cons A l ls0) ls) (@hlist_app A F (@cons A l ls0) ls (@Hcons A F l ls0 f x) xs) (@hlist_app A G (@cons A l ls0) ls (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y)) ys), and (@hlist_hrel A F G R (@cons A l ls0) (@Hcons A F l ls0 f x) (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y))) (@hlist_hrel A F G R ls xs ys) *)
    simpl. intros.
    match goal with
    | |- context [ match ?X with _ => _ end ] =>
      destruct X
(* Goal: @eq (G t) (@hlist_hd A G t ls (@hlist_map A F G ff (@cons A t ls) (@Hcons A F t ls (@hlist_hd A F t ls hl) (@hlist_tl A F t ls hl)))) (@ff t (@hlist_hd A F t ls (@Hcons A F t ls (@hlist_hd A F t ls hl) (@hlist_tl A F t ls hl)))) *)
    end. reflexivity.
  Qed.

  Lemma hlist_tl_fst_hlist_split
  : forall t (xs ys : list _) (h : hlist (t :: xs ++ ys)),
      hlist_tl (fst (hlist_split (t :: xs) ys h)) =
      fst (hlist_split xs ys (hlist_tl h)).
  Proof.
(* Goal: forall _ : @hlist_hrel A F G R (@app A (@cons A l ls0) ls) (@hlist_app A F (@cons A l ls0) ls (@Hcons A F l ls0 f x) xs) (@hlist_app A G (@cons A l ls0) ls (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y)) ys), and (@hlist_hrel A F G R (@cons A l ls0) (@Hcons A F l ls0 f x) (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y))) (@hlist_hrel A F G R ls xs ys) *)
    simpl. intros.
    match goal with
    | |- context [ match ?X with _ => _ end ] =>
      remember X
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) (@Hcons A F l ls (@hlist_hd A F l ls hl) (@hlist_tl A F l ls hl))))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls (@Hcons A F l ls (@hlist_hd A F l ls hl) (@hlist_tl A F l ls hl))))) *)
    end. destruct p. simpl.
(* Goal: @eq (hlist xs) h0 (@fst (hlist xs) (hlist ys) (hlist_split xs ys (@hlist_tl t (@app iT xs ys) h))) *)
    change h0 with (fst (h0, h1)).
(* Goal: @eq (hlist xs) (@fst (hlist xs) (hlist ys) (@pair (hlist xs) (hlist ys) h0 h1)) (@fst (hlist xs) (hlist ys) (hlist_split xs ys (@hlist_tl t (@app iT xs ys) h))) *)
    f_equal; trivial.
  Qed.

  Lemma hlist_tl_snd_hlist_split
  : forall t (xs ys : list _) (h : hlist (t :: xs ++ ys)),
      snd (hlist_split xs ys (hlist_tl h)) =
      snd (hlist_split (t :: xs) ys h).
  Proof.
(* Goal: forall _ : @hlist_hrel A F G R (@app A (@cons A l ls0) ls) (@hlist_app A F (@cons A l ls0) ls (@Hcons A F l ls0 f x) xs) (@hlist_app A G (@cons A l ls0) ls (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y)) ys), and (@hlist_hrel A F G R (@cons A l ls0) (@Hcons A F l ls0 f x) (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y))) (@hlist_hrel A F G R ls xs ys) *)
    simpl. intros.
    match goal with
    | |- context [ match ?X with _ => _ end ] =>
      remember X
(* Goal: @eq (hlist ys) (@snd (hlist xs) (hlist ys) (hlist_split xs ys (@hlist_tl t (@app iT xs ys) h))) (@snd (hlist (@cons iT t xs)) (hlist ys) (let (a, b) := p in @pair (hlist (@cons iT t xs)) (hlist ys) (@Hcons t xs (@hlist_hd t ((fix app (l m : list iT) {struct l} : list iT := match l with | nil => m | cons a0 l1 => @cons iT a0 (app l1 m) end) xs ys) h) a) b)) *)
    end. destruct p.
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) (@Hcons A F l ls (@hlist_hd A F l ls hl) (@hlist_tl A F l ls hl))))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls (@Hcons A F l ls (@hlist_hd A F l ls hl) (@hlist_tl A F l ls hl))))) *)
    simpl.
(* Goal: @eq (hlist ys) (@snd (hlist xs) (hlist ys) (hlist_split xs ys (@hlist_tl t (@app iT xs ys) h))) h1 *)
    change h1 with (snd (h0, h1)).
(* Goal: @eq (G t) (@hlist_hd A G t ls (@hlist_map A F G ff (@cons A t ls) (@Hcons A F t ls (@hlist_hd A F t ls hl) (@hlist_tl A F t ls hl)))) (@ff t (@hlist_hd A F t ls (@Hcons A F t ls (@hlist_hd A F t ls hl) (@hlist_tl A F t ls hl)))) *)
    rewrite Heqp. reflexivity.
  Qed.

(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
  Polymorphic Fixpoint nth_error_get_hlist_nth (ls : list iT) (n : nat) {struct ls} :
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
    option {t : iT & hlist ls -> F t} :=
    match
      ls as ls0
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
      return option {t : iT & hlist ls0 -> F t}
    with
      | nil => None
      | l :: ls0 =>
        match
          n as n0
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
          return option {t : iT & hlist (l :: ls0) -> F t}
        with
          | 0 =>
            Some (@existT _ (fun t => hlist (l :: ls0) -> F t)
                          l (@hlist_hd _ _))
          | S n0 =>
            match nth_error_get_hlist_nth ls0 n0 with
              | Some (existT x f) =>
                Some (@existT _ (fun t => hlist _ -> F t)
                              x (fun h : hlist (l :: ls0) => f (hlist_tl h)))
              | None => None
            end
        end
    end.

  Theorem nth_error_get_hlist_nth_Some
    : forall ls n s,
      nth_error_get_hlist_nth ls n = Some s ->
      exists pf : nth_error ls n = Some (projT1 s),
      forall h, projT2 s h = match pf in _ = t
                                   return match t return Type with
                                            | Some t => F t
                                            | None => unit
                                          end
                             with
                               | eq_refl => hlist_nth h n
                             end.
  Proof.
(* Goal: forall (ls : list iT) (n : nat) (x : @sigT iT (fun t : iT => forall _ : hlist ls, F t)) (_ : @eq (option (@sigT iT (fun t : iT => forall _ : hlist ls, F t))) (nth_error_get_hlist_nth ls n) (@Some (@sigT iT (fun t : iT => forall _ : hlist ls, F t)) x)), @ex (forall _ : hlist (@app iT ls ls'), F (@projT1 iT (fun t : iT => forall _ : hlist ls, F t) x)) (fun z : forall _ : hlist (@app iT ls ls'), F (@projT1 iT (fun t : iT => forall _ : hlist ls, F t) x) => and (@eq (option (@sigT iT (fun t : iT => forall _ : hlist (@app iT ls ls'), F t))) (nth_error_get_hlist_nth (@app iT ls ls') n) (@Some (@sigT iT (fun t : iT => forall _ : hlist (@app iT ls ls'), F t)) (@existT iT (fun t : iT => forall _ : hlist (@app iT ls ls'), F t) (@projT1 iT (fun t : iT => forall _ : hlist ls, F t) x) z))) (forall (h : hlist ls) (h' : hlist ls'), @eq (F (@projT1 iT (fun t : iT => forall _ : hlist ls, F t) x)) (@projT2 iT (fun t : iT => forall _ : hlist ls, F t) x h) (z (@hlist_app ls ls' h h')))) *)
    induction ls; simpl; intros; try congruence.
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
    { destruct n.
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
      { inv_all; subst; simpl.
(* Goal: @ex (@eq (option iT) (@Some iT a) (@Some iT a)) (fun pf : @eq (option iT) (@Some iT a) (@Some iT a) => forall h : hlist (@cons iT a ls), @eq (F a) (@hlist_hd a ls h) match pf in (eq _ t) return match t with | Some t0 => F t0 | None => unit end with | eq_refl => @hlist_nth (@cons iT a ls) h O end) *)
        exists (eq_refl).
(* Goal: @eq (G t) (@hlist_hd A G t ls (@hlist_map A F G ff (@cons A t ls) (@Hcons A F t ls (@hlist_hd A F t ls hl) (@hlist_tl A F t ls hl)))) (@ff t (@hlist_hd A F t ls (@Hcons A F t ls (@hlist_hd A F t ls hl) (@hlist_tl A F t ls hl)))) *)
        intros. rewrite (hlist_eta h). reflexivity. }
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
      { forward. inv_all; subst.
(* Goal: @ex (@eq (option iT) (@nth_error iT (@cons iT a ls) (S n)) (@Some iT (@projT1 iT (fun t : iT => forall _ : hlist (@cons iT a ls), F t) (@existT iT (fun t : iT => forall _ : hlist (@cons iT a ls), F t) x (fun h : hlist (@cons iT a ls) => f (@hlist_tl a ls h)))))) (fun pf : @eq (option iT) (@nth_error iT (@cons iT a ls) (S n)) (@Some iT (@projT1 iT (fun t : iT => forall _ : hlist (@cons iT a ls), F t) (@existT iT (fun t : iT => forall _ : hlist (@cons iT a ls), F t) x (fun h : hlist (@cons iT a ls) => f (@hlist_tl a ls h))))) => forall h : hlist (@cons iT a ls), @eq (F (@projT1 iT (fun t : iT => forall _ : hlist (@cons iT a ls), F t) (@existT iT (fun t : iT => forall _ : hlist (@cons iT a ls), F t) x (fun h0 : hlist (@cons iT a ls) => f (@hlist_tl a ls h0))))) (@projT2 iT (fun t : iT => forall _ : hlist (@cons iT a ls), F t) (@existT iT (fun t : iT => forall _ : hlist (@cons iT a ls), F t) x (fun h0 : hlist (@cons iT a ls) => f (@hlist_tl a ls h0))) h) match pf in (eq _ t) return match t with | Some t0 => F t0 | None => unit end with | eq_refl => @hlist_nth (@cons iT a ls) h (S n) end) *)
        destruct (IHls _ _ H0); clear IHls.
(* Goal: @ex (forall _ : hlist tvs', F x0) (fun y : forall _ : hlist tvs', F x0 => and (@eq (option (@sigT iT (fun t : iT => forall _ : hlist tvs', F t))) (nth_error_get_hlist_nth tvs' (Nat.sub n (@length iT tvs))) (@Some (@sigT iT (fun t : iT => forall _ : hlist tvs', F t)) (@existT iT (fun t : iT => forall _ : hlist tvs', F t) x0 y))) (forall (vs : hlist (@cons iT a tvs)) (vs' : hlist tvs'), @eq (F x0) (f (@hlist_tl a (@app iT tvs tvs') (@hlist_app (@cons iT a tvs) tvs' vs vs'))) (y vs'))) *)
        simpl in *. exists x0.
(* Goal: forall _ : @hlist_hrel A F G R (@app A (@cons A l ls0) ls) (@hlist_app A F (@cons A l ls0) ls (@Hcons A F l ls0 f x) xs) (@hlist_app A G (@cons A l ls0) ls (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y)) ys), and (@hlist_hrel A F G R (@cons A l ls0) (@Hcons A F l ls0 f x) (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y))) (@hlist_hrel A F G R ls xs ys) *)
        intros.
        rewrite (hlist_eta h). simpl. auto. } }
  Qed.

  Theorem nth_error_get_hlist_nth_None
  : forall ls n,
      nth_error_get_hlist_nth ls n = None <->
      nth_error ls n = None.
  Proof.
(* Goal: forall (ls : list iT) (n : nat) (x : @sigT iT (fun t : iT => forall _ : hlist ls, F t)) (_ : @eq (option (@sigT iT (fun t : iT => forall _ : hlist ls, F t))) (nth_error_get_hlist_nth ls n) (@Some (@sigT iT (fun t : iT => forall _ : hlist ls, F t)) x)), @ex (forall _ : hlist (@app iT ls ls'), F (@projT1 iT (fun t : iT => forall _ : hlist ls, F t) x)) (fun z : forall _ : hlist (@app iT ls ls'), F (@projT1 iT (fun t : iT => forall _ : hlist ls, F t) x) => and (@eq (option (@sigT iT (fun t : iT => forall _ : hlist (@app iT ls ls'), F t))) (nth_error_get_hlist_nth (@app iT ls ls') n) (@Some (@sigT iT (fun t : iT => forall _ : hlist (@app iT ls ls'), F t)) (@existT iT (fun t : iT => forall _ : hlist (@app iT ls ls'), F t) (@projT1 iT (fun t : iT => forall _ : hlist ls, F t) x) z))) (forall (h : hlist ls) (h' : hlist ls'), @eq (F (@projT1 iT (fun t : iT => forall _ : hlist ls, F t) x)) (@projT2 iT (fun t : iT => forall _ : hlist ls, F t) x h) (z (@hlist_app ls ls' h h')))) *)
    induction ls; simpl; intros; try congruence.
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
    { destruct n; intuition. }
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
    { destruct n; simpl; try solve [ intuition congruence ].
      specialize (IHls n). forward. }
  Qed.

  Lemma nth_error_get_hlist_nth_weaken
  : forall ls ls' n x,
      nth_error_get_hlist_nth ls n = Some x ->
      exists z,
        nth_error_get_hlist_nth (ls ++ ls') n =
        Some (@existT iT (fun t => hlist (ls ++ ls') -> F t) (projT1 x) z)
        /\ forall h h', projT2 x h = z (hlist_app h h').
  Proof.
(* Goal: forall (ls ls' : list iT) (n : nat) (x : @sigT iT (fun t : iT => forall _ : hlist ls, F t)) (_ : @eq (option (@sigT iT (fun t : iT => forall _ : hlist ls, F t))) (nth_error_get_hlist_nth ls n) (@Some (@sigT iT (fun t : iT => forall _ : hlist ls, F t)) x)), @ex (forall _ : hlist (@app iT ls ls'), F (@projT1 iT (fun t : iT => forall _ : hlist ls, F t) x)) (fun z : forall _ : hlist (@app iT ls ls'), F (@projT1 iT (fun t : iT => forall _ : hlist ls, F t) x) => and (@eq (option (@sigT iT (fun t : iT => forall _ : hlist (@app iT ls ls'), F t))) (nth_error_get_hlist_nth (@app iT ls ls') n) (@Some (@sigT iT (fun t : iT => forall _ : hlist (@app iT ls ls'), F t)) (@existT iT (fun t : iT => forall _ : hlist (@app iT ls ls'), F t) (@projT1 iT (fun t : iT => forall _ : hlist ls, F t) x) z))) (forall (h : hlist ls) (h' : hlist ls'), @eq (F (@projT1 iT (fun t : iT => forall _ : hlist ls, F t) x)) (@projT2 iT (fun t : iT => forall _ : hlist ls, F t) x h) (z (@hlist_app ls ls' h h')))) *)
    intros ls ls'. revert ls.
(* Goal: forall (ls : list iT) (n : nat) (x : @sigT iT (fun t : iT => forall _ : hlist ls, F t)) (_ : @eq (option (@sigT iT (fun t : iT => forall _ : hlist ls, F t))) (nth_error_get_hlist_nth ls n) (@Some (@sigT iT (fun t : iT => forall _ : hlist ls, F t)) x)), @ex (forall _ : hlist (@app iT ls ls'), F (@projT1 iT (fun t : iT => forall _ : hlist ls, F t) x)) (fun z : forall _ : hlist (@app iT ls ls'), F (@projT1 iT (fun t : iT => forall _ : hlist ls, F t) x) => and (@eq (option (@sigT iT (fun t : iT => forall _ : hlist (@app iT ls ls'), F t))) (nth_error_get_hlist_nth (@app iT ls ls') n) (@Some (@sigT iT (fun t : iT => forall _ : hlist (@app iT ls ls'), F t)) (@existT iT (fun t : iT => forall _ : hlist (@app iT ls ls'), F t) (@projT1 iT (fun t : iT => forall _ : hlist ls, F t) x) z))) (forall (h : hlist ls) (h' : hlist ls'), @eq (F (@projT1 iT (fun t : iT => forall _ : hlist ls, F t) x)) (@projT2 iT (fun t : iT => forall _ : hlist ls, F t) x h) (z (@hlist_app ls ls' h h')))) *)
    induction ls; simpl; intros; try congruence.
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
    { destruct n; inv_all; subst.
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
      { simpl. eexists; split; eauto.
(* Goal: @eq (G t) (@hlist_hd A G t ls (@hlist_map A F G ff (@cons A t ls) (@Hcons A F t ls (@hlist_hd A F t ls hl) (@hlist_tl A F t ls hl)))) (@ff t (@hlist_hd A F t ls (@Hcons A F t ls (@hlist_hd A F t ls hl) (@hlist_tl A F t ls hl)))) *)
        intros. rewrite (hlist_eta h). reflexivity. }
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
      { forward. inv_all; subst. simpl.
(* Goal: @ex (forall _ : hlist (@cons iT a (@app iT ls ls')), F x0) (fun z : forall _ : hlist (@cons iT a (@app iT ls ls')), F x0 => and (@eq (option (@sigT iT (fun t : iT => forall _ : hlist (@cons iT a (@app iT ls ls')), F t))) match nth_error_get_hlist_nth (@app iT ls ls') n with | Some (@existT _ _ x f as s) => @Some (@sigT iT (fun t : iT => forall _ : hlist (@cons iT a (@app iT ls ls')), F t)) (@existT iT (fun t : iT => forall _ : hlist (@cons iT a (@app iT ls ls')), F t) x (fun h : hlist (@cons iT a (@app iT ls ls')) => f (@hlist_tl a (@app iT ls ls') h))) | None => @None (@sigT iT (fun t : iT => forall _ : hlist (@cons iT a (@app iT ls ls')), F t)) end (@Some (@sigT iT (fun t : iT => forall _ : hlist (@cons iT a (@app iT ls ls')), F t)) (@existT iT (fun t : iT => forall _ : hlist (@cons iT a (@app iT ls ls')), F t) x0 z))) (forall (h : hlist (@cons iT a ls)) (h' : hlist ls'), @eq (F x0) (f (@hlist_tl a ls h)) (z (@hlist_app (@cons iT a ls) ls' h h')))) *)
        apply IHls in H0. forward_reason.
(* Goal: forall t : A, R t (x t) (y t) *)
        rewrite H. eexists; split; eauto.
(* Goal: forall _ : @hlist_hrel A F G R (@app A (@cons A l ls0) ls) (@hlist_app A F (@cons A l ls0) ls (@Hcons A F l ls0 f x) xs) (@hlist_app A G (@cons A l ls0) ls (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y)) ys), and (@hlist_hrel A F G R (@cons A l ls0) (@Hcons A F l ls0 f x) (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y))) (@hlist_hrel A F G R ls xs ys) *)
        intros. rewrite (hlist_eta h). simpl in *.
        auto. } }
  Qed.

  Lemma nth_error_get_hlist_nth_appL
  : forall tvs' tvs n,
      n < length tvs ->
      exists x,
        nth_error_get_hlist_nth (tvs ++ tvs') n = Some x /\
        exists y,
          nth_error_get_hlist_nth tvs n = Some (@existT _ _ (projT1 x) y) /\
          forall vs vs',
            (projT2 x) (hlist_app vs vs') = y vs.
  Proof.
(* Goal: forall _ : @hlist_hrel A F G R (@app A (@cons A l ls0) ls) (@hlist_app A F (@cons A l ls0) ls (@Hcons A F l ls0 f x) xs) (@hlist_app A G (@cons A l ls0) ls (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y)) ys), and (@hlist_hrel A F G R (@cons A l ls0) (@Hcons A F l ls0 f x) (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y))) (@hlist_hrel A F G R ls xs ys) *)
    clear. induction tvs; simpl; intros.
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
    { exfalso; inversion H. }
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
    { destruct n.
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
      { clear H IHtvs.
(* Goal: forall t : A, R t (x t) (y t) *)
        eexists; split; eauto. eexists; split; eauto.
(* Goal: @eq (G t) (@hlist_hd A G t ls (@hlist_map A F G ff (@cons A t ls) (@Hcons A F t ls (@hlist_hd A F t ls hl) (@hlist_tl A F t ls hl)))) (@ff t (@hlist_hd A F t ls (@Hcons A F t ls (@hlist_hd A F t ls hl) (@hlist_tl A F t ls hl)))) *)
        simpl. intros. rewrite (hlist_eta vs). reflexivity. }
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
      { apply Lt.lt_S_n in H.
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
        { specialize (IHtvs _ H).
(* Goal: @ex (forall _ : hlist tvs', F x0) (fun y : forall _ : hlist tvs', F x0 => and (@eq (option (@sigT iT (fun t : iT => forall _ : hlist tvs', F t))) (nth_error_get_hlist_nth tvs' (Nat.sub n (@length iT tvs))) (@Some (@sigT iT (fun t : iT => forall _ : hlist tvs', F t)) (@existT iT (fun t : iT => forall _ : hlist tvs', F t) x0 y))) (forall (vs : hlist (@cons iT a tvs)) (vs' : hlist tvs'), @eq (F x0) (f (@hlist_tl a (@app iT tvs tvs') (@hlist_app (@cons iT a tvs) tvs' vs vs'))) (y vs'))) *)
          forward_reason.
(* Goal: @ex (forall _ : hlist tvs', F (@projT1 iT (fun t : iT => forall _ : hlist tvs', F t) x)) (fun y : forall _ : hlist tvs', F (@projT1 iT (fun t : iT => forall _ : hlist tvs', F t) x) => and (@eq (option (@sigT iT (fun t : iT => forall _ : hlist tvs', F t))) (nth_error_get_hlist_nth tvs' n) (@Some (@sigT iT (fun t : iT => forall _ : hlist tvs', F t)) (@existT iT (fun t : iT => forall _ : hlist tvs', F t) (@projT1 iT (fun t : iT => forall _ : hlist tvs', F t) x) y))) (forall (vs : hlist (@nil iT)) (vs' : hlist tvs'), @eq (F (@projT1 iT (fun t : iT => forall _ : hlist tvs', F t) x)) (@projT2 iT (fun t : iT => forall _ : hlist tvs', F t) x (@hlist_app (@nil iT) tvs' vs vs')) (y vs'))) *)
          rewrite H0. rewrite H1.
(* Goal: @ex (forall _ : hlist tvs', F x0) (fun y : forall _ : hlist tvs', F x0 => and (@eq (option (@sigT iT (fun t : iT => forall _ : hlist tvs', F t))) (nth_error_get_hlist_nth tvs' (Nat.sub n (@length iT tvs))) (@Some (@sigT iT (fun t : iT => forall _ : hlist tvs', F t)) (@existT iT (fun t : iT => forall _ : hlist tvs', F t) x0 y))) (forall (vs : hlist (@cons iT a tvs)) (vs' : hlist tvs'), @eq (F x0) (f (@hlist_tl a (@app iT tvs tvs') (@hlist_app (@cons iT a tvs) tvs' vs vs'))) (y vs'))) *)
          forward. subst. simpl in *.
(* Goal: forall t : A, R t (x t) (y t) *)
          eexists; split; eauto.
(* Goal: forall t : A, R t (x t) (y t) *)
          eexists; split; eauto. simpl.
(* Goal: forall _ : @hlist_hrel A F G R (@app A (@cons A l ls0) ls) (@hlist_app A F (@cons A l ls0) ls (@Hcons A F l ls0 f x) xs) (@hlist_app A G (@cons A l ls0) ls (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y)) ys), and (@hlist_hrel A F G R (@cons A l ls0) (@Hcons A F l ls0 f x) (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y))) (@hlist_hrel A F G R ls xs ys) *)
          intros. rewrite (hlist_eta vs). simpl. auto. } } }
  Qed.

  Lemma nth_error_get_hlist_nth_appR
  : forall tvs' tvs n x,
      n >= length tvs ->
      nth_error_get_hlist_nth (tvs ++ tvs') n = Some x ->
      exists y,
        nth_error_get_hlist_nth tvs' (n - length tvs) = Some (@existT _ _ (projT1 x) y) /\
        forall vs vs',
          (projT2 x) (hlist_app vs vs') = y vs'.
  Proof.
(* Goal: forall _ : @hlist_hrel A F G R (@app A (@cons A l ls0) ls) (@hlist_app A F (@cons A l ls0) ls (@Hcons A F l ls0 f x) xs) (@hlist_app A G (@cons A l ls0) ls (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y)) ys), and (@hlist_hrel A F G R (@cons A l ls0) (@Hcons A F l ls0 f x) (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y))) (@hlist_hrel A F G R ls xs ys) *)
    clear. induction tvs; simpl; intros.
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
    { rewrite <- Minus.minus_n_O.
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) (@Hcons A F l ls (@hlist_hd A F l ls hl) (@hlist_tl A F l ls hl))))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls (@Hcons A F l ls (@hlist_hd A F l ls hl) (@hlist_tl A F l ls hl))))) *)
      rewrite H0. destruct x. simpl.
(* Goal: forall _ : @hlist_hrel A F G R (@app A (@cons A l ls0) ls) (@hlist_app A F (@cons A l ls0) ls (@Hcons A F l ls0 f x) xs) (@hlist_app A G (@cons A l ls0) ls (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y)) ys), and (@hlist_hrel A F G R (@cons A l ls0) (@Hcons A F l ls0 f x) (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y))) (@hlist_hrel A F G R ls xs ys) *)
      eexists; split; eauto. intros.
(* Goal: @eq (G t) (@hlist_hd A G t ls (@hlist_map A F G ff (@cons A t ls) (@Hcons A F t ls (@hlist_hd A F t ls hl) (@hlist_tl A F t ls hl)))) (@ff t (@hlist_hd A F t ls (@Hcons A F t ls (@hlist_hd A F t ls hl) (@hlist_tl A F t ls hl)))) *)
      rewrite (hlist_eta vs). reflexivity. }
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
    { destruct n.
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
      { inversion H. }
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
      { assert (n >= length tvs) by (eapply le_S_n; eassumption). clear H.
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
        { forward. inv_all; subst. simpl in *.
(* Goal: @ex (forall _ : hlist tvs', F x0) (fun y : forall _ : hlist tvs', F x0 => and (@eq (option (@sigT iT (fun t : iT => forall _ : hlist tvs', F t))) (nth_error_get_hlist_nth tvs' (Nat.sub n (@length iT tvs))) (@Some (@sigT iT (fun t : iT => forall _ : hlist tvs', F t)) (@existT iT (fun t : iT => forall _ : hlist tvs', F t) x0 y))) (forall (vs : hlist (@cons iT a tvs)) (vs' : hlist tvs'), @eq (F x0) (f (@hlist_tl a (@app iT tvs tvs') (@hlist_app (@cons iT a tvs) tvs' vs vs'))) (y vs'))) *)
          specialize (IHtvs _ _ H1 H0).
(* Goal: @ex (forall _ : hlist tvs', F x0) (fun y : forall _ : hlist tvs', F x0 => and (@eq (option (@sigT iT (fun t : iT => forall _ : hlist tvs', F t))) (nth_error_get_hlist_nth tvs' (Nat.sub n (@length iT tvs))) (@Some (@sigT iT (fun t : iT => forall _ : hlist tvs', F t)) (@existT iT (fun t : iT => forall _ : hlist tvs', F t) x0 y))) (forall (vs : hlist (@cons iT a tvs)) (vs' : hlist tvs'), @eq (F x0) (f (@hlist_tl a (@app iT tvs tvs') (@hlist_app (@cons iT a tvs) tvs' vs vs'))) (y vs'))) *)
          simpl in *.
(* Goal: @ex (forall _ : hlist tvs', F x0) (fun y : forall _ : hlist tvs', F x0 => and (@eq (option (@sigT iT (fun t : iT => forall _ : hlist tvs', F t))) (nth_error_get_hlist_nth tvs' (Nat.sub n (@length iT tvs))) (@Some (@sigT iT (fun t : iT => forall _ : hlist tvs', F t)) (@existT iT (fun t : iT => forall _ : hlist tvs', F t) x0 y))) (forall (vs : hlist (@cons iT a tvs)) (vs' : hlist tvs'), @eq (F x0) (f (@hlist_tl a (@app iT tvs tvs') (@hlist_app (@cons iT a tvs) tvs' vs vs'))) (y vs'))) *)
          forward_reason.
(* Goal: @ex (forall _ : hlist tvs', F x0) (fun y : forall _ : hlist tvs', F x0 => and (@eq (option (@sigT iT (fun t : iT => forall _ : hlist tvs', F t))) (nth_error_get_hlist_nth tvs' (Nat.sub n (@length iT tvs))) (@Some (@sigT iT (fun t : iT => forall _ : hlist tvs', F t)) (@existT iT (fun t : iT => forall _ : hlist tvs', F t) x0 y))) (forall (vs : hlist (@cons iT a tvs)) (vs' : hlist tvs'), @eq (F x0) (f (@hlist_tl a (@app iT tvs tvs') (@hlist_app (@cons iT a tvs) tvs' vs vs'))) (y vs'))) *)
          rewrite H.
(* Goal: forall t : A, R t (x t) (y t) *)
          eexists; split; eauto.
(* Goal: forall _ : @hlist_hrel A F G R (@app A (@cons A l ls0) ls) (@hlist_app A F (@cons A l ls0) ls (@Hcons A F l ls0 f x) xs) (@hlist_app A G (@cons A l ls0) ls (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y)) ys), and (@hlist_hrel A F G R (@cons A l ls0) (@Hcons A F l ls0 f x) (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y))) (@hlist_hrel A F G R ls xs ys) *)
          intros. rewrite (hlist_eta vs). simpl. auto. } } }
  Qed.

End hlist.

(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
Arguments Hnil {_ _}.
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
Arguments Hcons {_ _ _ _} _ _.
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
Arguments equiv_hlist {_ F} R {_} _ _ : rename.

(** Weak Map
 ** This is weak because it does not change the key type
 **)
Section hlist_map.
  Variable A : Type.
  Variables F G : A -> Type.
  Variable ff : forall x, F x -> G x.

(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
  Fixpoint hlist_map (ls : list A) (hl : hlist F ls) {struct hl} : hlist G ls :=
    match hl in @hlist _ _ ls return hlist G ls with
      | Hnil => Hnil
      | Hcons _ _ hd tl =>
        Hcons (ff hd) (hlist_map tl)
    end.

  Theorem hlist_app_hlist_map
    : forall ls ls' (a : hlist F ls) (b : hlist F ls'),
      hlist_map (hlist_app a b) =
      hlist_app (hlist_map a) (hlist_map b).
  Proof.
(* Goal: forall t : A, R t (x t) (y t) *)
    induction a. simpl; auto.
(* Goal: forall _ : @hlist_hrel A F G R (@app A (@cons A l ls0) ls) (@hlist_app A F (@cons A l ls0) ls (@Hcons A F l ls0 f x) xs) (@hlist_app A G (@cons A l ls0) ls (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y)) ys), and (@hlist_hrel A F G R (@cons A l ls0) (@Hcons A F l ls0 f x) (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y))) (@hlist_hrel A F G R ls xs ys) *)
    simpl. intros. f_equal. auto.
  Qed.

End hlist_map.

(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
Arguments hlist_map {_ _ _} _ {_} _.


Section hlist_map_rules.
  Variable A : Type.
  Variables F G G' : A -> Type.
  Variable ff : forall x, F x -> G x.
  Variable gg : forall x, G x -> G' x.

  Theorem hlist_map_hlist_map : forall ls (hl : hlist F ls),
      hlist_map gg (hlist_map ff hl) = hlist_map (fun _ x => gg (ff x)) hl.
  Proof.
(* Goal: @eq (@hlist A G' ls) (@hlist_map A G G' gg ls (@hlist_map A F G ff ls hl)) (@hlist_map A (fun H : A => F H) (fun H : A => G' H) (fun (x : A) (x0 : F x) => @gg x (@ff x x0)) ls hl) *)
    induction hl; simpl; f_equal. assumption.
  Defined.

  Theorem hlist_get_hlist_map : forall ls t (hl : hlist F ls) (m : member t ls),
      hlist_get m (hlist_map ff hl) = ff (hlist_get m hl).
  Proof.
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) (@Hcons A F l ls (@hlist_hd A F l ls hl) (@hlist_tl A F l ls hl))))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls (@Hcons A F l ls (@hlist_hd A F l ls hl) (@hlist_tl A F l ls hl))))) *)
    induction m; simpl.
(* Goal: @eq (G t) (@hlist_hd A G t ls (@hlist_map A F G ff (@cons A t ls) (@Hcons A F t ls (@hlist_hd A F t ls hl) (@hlist_tl A F t ls hl)))) (@ff t (@hlist_hd A F t ls (@Hcons A F t ls (@hlist_hd A F t ls hl) (@hlist_tl A F t ls hl)))) *)
    { rewrite (hlist_eta hl). reflexivity. }
(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
    { rewrite (hlist_eta hl). simpl. auto. }
  Defined.

  Lemma hlist_map_ext : forall (ff gg : forall x, F x -> G x),
      (forall x t, ff x t = gg x t) ->
      forall ls (hl : hlist F ls),
        hlist_map ff hl = hlist_map gg hl.
  Proof.
(* Goal: forall t : A, R t (x t) (y t) *)
    induction hl; simpl; auto.
(* Goal: forall _ : @hlist_hrel A F G R (@app A (@cons A l ls0) ls) (@hlist_app A F (@cons A l ls0) ls (@Hcons A F l ls0 f x) xs) (@hlist_app A G (@cons A l ls0) ls (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y)) ys), and (@hlist_hrel A F G R (@cons A l ls0) (@Hcons A F l ls0 f x) (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y))) (@hlist_hrel A F G R ls xs ys) *)
    intros. f_equal; auto.
  Defined.

End hlist_map_rules.

Lemma equiv_hlist_map
: forall T U (F : T -> Type) (R : forall t, F t -> F t -> Prop)
         (R' : forall t, U t -> U t -> Prop)
         (f g : forall t, F t -> U t),
    (forall t (x y : F t), R t x y -> R' t (f t x) (g t y)) ->
    forall  ls (a b : hlist F ls),
      equiv_hlist R a b ->
      equiv_hlist R' (hlist_map f a) (hlist_map g b).
Proof.
(* Goal: forall _ : @hlist_hrel A F G R (@app A (@cons A l ls0) ls) (@hlist_app A F (@cons A l ls0) ls (@Hcons A F l ls0 f x) xs) (@hlist_app A G (@cons A l ls0) ls (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y)) ys), and (@hlist_hrel A F G R (@cons A l ls0) (@Hcons A F l ls0 f x) (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y))) (@hlist_hrel A F G R ls xs ys) *)
  clear. induction 2; simpl; intros.
(* Goal: @hlist_hrel A F G R (@nil A) (@Hnil A F) (@Hnil A G) *)
  - constructor.
(* Goal: forall t : A, R t (x t) (y t) *)
  - constructor; eauto.
Qed.


(** Linking Heterogeneous Lists and Lists **)

Section hlist_gen.
  Variable A : Type.
  Variable F : A -> Type.
  Variable f : forall a, F a.

  Fixpoint hlist_gen ls : hlist F ls :=
    match ls with
    | nil => Hnil
    | cons x ls' => Hcons (f x) (hlist_gen ls')
    end.

  Lemma hlist_get_hlist_gen : forall ls t (m : member t ls),
    hlist_get m (hlist_gen ls) = f t.
  Proof.
(* Goal: forall t : A, R t (x t) (y t) *)
    induction m; simpl; auto.
  Qed.

  (** This function is a generalisation of [hlist_gen] in which the function [f]
    takes the additional parameter [member a ls]. **)
  Fixpoint hlist_gen_member ls : (forall a, member a ls -> F a) -> hlist F ls :=
    match ls as ls return ((forall a : A, member a ls -> F a) -> hlist F ls) with
    | nil => fun _ => Hnil
    | a :: ls' => fun fm =>
        Hcons (fm a (MZ a ls'))
          (hlist_gen_member (fun a' (M : member a' ls') => fm a' (MN a M)))
    end.

  Lemma hlist_gen_member_hlist_gen : forall ls,
    hlist_gen_member (fun a _ => f a) = hlist_gen ls.
  Proof.
(* Goal: forall t : A, R t (x t) (y t) *)
    induction ls; simpl; f_equal; auto.
  Qed.

  Lemma hlist_gen_member_ext : forall ls (f g : forall a, member a ls -> F a),
    (forall x M, f x M = g x M) ->
    hlist_gen_member f = hlist_gen_member g.
  Proof.
(* Goal: forall _ : @hlist_hrel A F G R (@app A (@cons A l ls0) ls) (@hlist_app A F (@cons A l ls0) ls (@Hcons A F l ls0 f x) xs) (@hlist_app A G (@cons A l ls0) ls (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y)) ys), and (@hlist_hrel A F G R (@cons A l ls0) (@Hcons A F l ls0 f x) (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y))) (@hlist_hrel A F G R ls xs ys) *)
    intros. induction ls; simpl; f_equal; auto.
  Qed.

End hlist_gen.

(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
Arguments hlist_gen {A F} f ls.

Lemma hlist_gen_member_hlist_map : forall A (F G : A -> Type) (ff : forall t, F t -> G t) ls f,
  hlist_map ff (hlist_gen_member F (ls := ls) f) = hlist_gen_member G (fun a M => ff _ (f _ M)).
Proof.
(* Goal: forall _ : @hlist_hrel A F G R (@app A (@cons A l ls0) ls) (@hlist_app A F (@cons A l ls0) ls (@Hcons A F l ls0 f x) xs) (@hlist_app A G (@cons A l ls0) ls (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y)) ys), and (@hlist_hrel A F G R (@cons A l ls0) (@Hcons A F l ls0 f x) (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y))) (@hlist_hrel A F G R ls xs ys) *)
  intros. induction ls; simpl; f_equal; auto.
Qed.

Lemma hlist_gen_hlist_map : forall A (F G : A -> Type) (ff : forall t, F t -> G t) f ls,
  hlist_map ff (hlist_gen f ls) = hlist_gen (fun a => ff _ (f a)) ls.
Proof.
(* Goal: forall _ : @hlist_hrel A F G R (@app A (@cons A l ls0) ls) (@hlist_app A F (@cons A l ls0) ls (@Hcons A F l ls0 f x) xs) (@hlist_app A G (@cons A l ls0) ls (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y)) ys), and (@hlist_hrel A F G R (@cons A l ls0) (@Hcons A F l ls0 f x) (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y))) (@hlist_hrel A F G R ls xs ys) *)
  intros. do 2 rewrite <- hlist_gen_member_hlist_gen. apply hlist_gen_member_hlist_map.
Qed.

Lemma hlist_gen_ext : forall A F (f g : forall a, F a),
  (forall x, f x = g x) ->
  forall ls : list A, hlist_gen f ls = hlist_gen g ls.
Proof.
(* Goal: forall _ : @hlist_hrel A F G R (@app A (@cons A l ls0) ls) (@hlist_app A F (@cons A l ls0) ls (@Hcons A F l ls0 f x) xs) (@hlist_app A G (@cons A l ls0) ls (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y)) ys), and (@hlist_hrel A F G R (@cons A l ls0) (@Hcons A F l ls0 f x) (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y))) (@hlist_hrel A F G R ls xs ys) *)
  intros. do 2 rewrite <- hlist_gen_member_hlist_gen. apply hlist_gen_member_ext. auto.
Qed.

Global Instance Proper_hlist_gen : forall A F,
  Proper (forall_relation (fun _ => eq) ==> forall_relation (fun _ => eq))
         (@hlist_gen A F).
Proof.
(* Goal: forall t : A, R t (x t) (y t) *)
  repeat intro. apply hlist_gen_ext. auto.
Qed.

Lemma equiv_hlist_gen : forall T (F : T -> Type) (f : forall t, F t) f'
    (R : forall t, F t -> F t -> Prop),
  (forall t, R t (f t) (f' t)) ->
  forall ls,
    equiv_hlist R (hlist_gen f ls) (hlist_gen f' ls).
Proof.
(* Goal: forall t : A, R t (x t) (y t) *)
  induction ls; simpl; constructor; auto.
Qed.

Global Instance Proper_equiv_hlist_gen : forall A (F : A -> Type) R,
  Proper (forall_relation R ==> forall_relation (@equiv_hlist _ _ R))
         (@hlist_gen A F).
Proof.
(* Goal: forall t : A, R t (x t) (y t) *)
  repeat intro. apply equiv_hlist_gen. auto.
Qed.

(* Goal: @eq (G t) (@hlist_get A G ls t m (@hlist_tl A G l ls (@hlist_map A F G ff (@cons A l ls) hl))) (@ff t (@hlist_get A F ls t m (@hlist_tl A F l ls hl))) *)
Fixpoint hlist_erase {A B} {ls : list A} (hs : hlist (fun _ => B) ls) : list B :=
  match hs with
  | Hnil => nil
  | Hcons _ _ x hs' => cons x (hlist_erase hs')
  end.

Lemma hlist_erase_hlist_gen : forall A B ls (f : A -> B),
  hlist_erase (hlist_gen f ls) = map f ls.
Proof.
(* Goal: forall t : A, R t (x t) (y t) *)
  induction ls; simpl; intros; f_equal; auto.
Qed.


(** Linking Heterogeneous Lists and Predicates **)

Section hlist_Forall.
  Variable A : Type.
  Variable P : A -> Prop.

  Fixpoint hlist_Forall ls (hs : hlist P ls) : Forall P ls :=
    match hs with
    | Hnil => Forall_nil _
    | Hcons _ _ H hs' => Forall_cons _ H (hlist_Forall hs')
    end.

End hlist_Forall.


(** Heterogeneous Relations **)
Section hlist_rel.
  Variable A : Type.
  Variables F G : A -> Type.
  Variable R : forall x : A, F x -> G x -> Prop.

  Inductive hlist_hrel : forall ls, hlist F ls -> hlist G ls -> Prop :=
  | hrel_Hnil : hlist_hrel Hnil Hnil
  | hrel_Hcons : forall t ts x y xs ys, @R t x y -> @hlist_hrel ts xs ys ->
                                        @hlist_hrel (t :: ts) (Hcons x xs) (Hcons y ys).

End hlist_rel.

Section hlist_rel_map.
  Variable A : Type.
  Variables F G F' G' : A -> Type.
  Variable R : forall x : A, F x -> G x -> Prop.
  Variable R' : forall x : A, F' x -> G' x -> Prop.
  Variable ff : forall x : A, F x -> F' x.
  Variable gg : forall x : A, G x -> G' x.

  Hypothesis R_ff_R' :
    forall t x y, @R t x y ->
                  @R' t (ff x) (gg y).

  Theorem hlist_hrel_map
  : forall ls xs ys,
      @hlist_hrel A F G R ls xs ys ->
      @hlist_hrel A F' G' R' ls (hlist_map ff xs) (hlist_map gg ys).
  Proof.
(* Goal: forall t : A, R t (x t) (y t) *)
    induction 1; simpl; constructor; eauto.
  Qed.

  Theorem hlist_hrel_cons
  : forall l ls x xs y ys,
      @hlist_hrel A F G R (l :: ls) (Hcons x xs) (Hcons y ys) ->
      @R l x y /\ @hlist_hrel A F G R ls xs ys.
  Proof.
(* Goal: forall _ : @hlist_hrel A F G R (@app A (@cons A l ls0) ls) (@hlist_app A F (@cons A l ls0) ls (@Hcons A F l ls0 f x) xs) (@hlist_app A G (@cons A l ls0) ls (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y)) ys), and (@hlist_hrel A F G R (@cons A l ls0) (@Hcons A F l ls0 f x) (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y))) (@hlist_hrel A F G R ls xs ys) *)
    intros.
    refine
      match H in @hlist_hrel _ _ _ _ ls' xs' ys'
            return
            match ls' as ls' return hlist F ls' -> hlist G ls' -> Prop with
              | nil => fun _ _ => True
              | l' :: ls' => fun x y =>
                   R (hlist_hd x) (hlist_hd y)
                /\ hlist_hrel R (hlist_tl x) (hlist_tl y)
            end xs' ys'
      with
        | hrel_Hnil => I
        | hrel_Hcons _ _ _ _ _ _ pf pf' => conj pf pf'
      end.
  Qed.

  Theorem hlist_hrel_app
  : forall l ls x xs y ys,
      @hlist_hrel A F G R (l ++ ls) (hlist_app x xs) (hlist_app y ys) ->
      @hlist_hrel A F G R l x y /\ @hlist_hrel A F G R ls xs ys.
  Proof.
(* Goal: forall (l ls : list A) (x : @hlist A F l) (xs : @hlist A F ls) (y : @hlist A G l) (ys : @hlist A G ls) (_ : @hlist_hrel A F G R (@app A l ls) (@hlist_app A F l ls x xs) (@hlist_app A G l ls y ys)), and (@hlist_hrel A F G R l x y) (@hlist_hrel A F G R ls xs ys) *)
    induction x.
    + intros xs y ys. rewrite (hlist_eta y).
(* Goal: @hlist_hrel A F G R (@nil A) (@Hnil A F) (@Hnil A G) *)
      simpl; intros; split; auto. constructor.
    + intros xs y ys. rewrite (hlist_eta y).
(* Goal: forall _ : @hlist_hrel A F G R (@app A (@cons A l ls0) ls) (@hlist_app A F (@cons A l ls0) ls (@Hcons A F l ls0 f x) xs) (@hlist_app A G (@cons A l ls0) ls (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y)) ys), and (@hlist_hrel A F G R (@cons A l ls0) (@Hcons A F l ls0 f x) (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y))) (@hlist_hrel A F G R ls xs ys) *)
      intros. eapply hlist_hrel_cons in H.
(* Goal: and (@hlist_hrel A F G R (@cons A l ls0) (@Hcons A F l ls0 f x) (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y))) (@hlist_hrel A F G R ls xs ys) *)
      destruct H.
(* Goal: and (@hlist_hrel A F G R (@cons A l ls0) (@Hcons A F l ls0 f x) (@Hcons A G l ls0 (@hlist_hd A G l ls0 y) (@hlist_tl A G l ls0 y))) (@hlist_hrel A F G R ls xs ys) *)
      apply IHx in H0.
(* Goal: forall t : A, R t (x t) (y t) *)
      intuition. constructor; auto.
  Qed.

End hlist_rel_map.

Theorem hlist_hrel_equiv
: forall T (F : T -> Type) (R : forall t, F t -> F t -> Prop) ls (h h' : hlist F ls),
    hlist_hrel R h h' ->
    equiv_hlist R h h'.
Proof.
(* Goal: forall t : A, R t (x t) (y t) *)
  induction 1; constructor; auto.
Qed.

Theorem hlist_hrel_flip
: forall T (F G : T -> Type) (R : forall t, F t -> G t -> Prop) ls
         (h : hlist F ls) (h' : hlist G ls),
    hlist_hrel R h h' ->
    hlist_hrel (fun t a b => R t b a) h' h.
Proof.
(* Goal: forall t : A, R t (x t) (y t) *)
  induction 1; constructor; auto.
Qed.
