3 files changed, 34 insertions, 13 deletions
diff --git a/_CoqProject b/_CoqProject
index 48d7d72b0..febc3c5b7 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -165,6 +165,7 @@ src/Util/Decidable.v
 src/Util/Equality.v
 src/Util/FixCoqMistakes.v
 src/Util/GlobalSettings.v
+src/Util/HList.v
 src/Util/HProp.v
 src/Util/Isomorphism.v
 src/Util/IterAssocOp.v
diff --git a/src/Util/HList.v b/src/Util/HList.v
new file mode 100644
index 000000000..addb0e40d
--- /dev/null
+++ b/src/Util/HList.v
@@ -0,0 +1,33 @@
+Require Import Coq.Classes.Morphisms.
+Require Import Coq.Relations.Relation_Definitions.
+Require Import Coq.Lists.List.
+Require Import Crypto.Util.Decidable.
+Require Import Crypto.Util.ListUtil.
+Require Import Crypto.Util.Tuple.
+Require Export Crypto.Util.FixCoqMistakes.
+
+Fixpoint hlist' T n (f : T -> Type) : tuple' T n -> Type :=
+  match n return tuple' _ n -> Type with
+  | 0 => fun T => f T
+  | S n' => fun Ts => (hlist' T n' f (fst Ts) * f (snd Ts))%type
+  end.
+Global Arguments hlist' {T n} f _.
+
+Definition hlist {T n} (f : T -> Type) : forall (Ts : tuple T n), Type :=
+  match n return tuple _ n -> Type with
+  | 0 => fun _ => unit
+  | S n' => @hlist' T n' f
+  end.
+
+(* tuple map *)
+Fixpoint mapt' {n A F B} (f : forall x : A, F x -> B) : forall ts : tuple' A n, hlist' F ts -> tuple' B n
+  := match n return forall ts : tuple' A n, hlist' F ts -> tuple' B n with
+     | 0 => fun ts v => f _ v
+     | S n' => fun ts v => (@mapt' n' A F B f _ (fst v), f _ (snd v))
+     end.
+Definition mapt {n A F B} (f : forall x : A, F x -> B)
+  : forall ts : tuple A n, hlist F ts -> tuple B n
+  := match n return forall ts : tuple A n, hlist F ts -> tuple B n with
+     | 0 => fun ts v => tt
+     | S n' => @mapt' n' A F B f
+     end.
diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v
index 65f1f868e..2e9f7b0ad 100644
--- a/src/Util/Tuple.v
+++ b/src/Util/Tuple.v
@@ -17,19 +17,6 @@ Definition tuple T n : Type :=
   | S n' => tuple' T n'
   end.
 
-Fixpoint hlist' T n (f : T -> Type) : tuple' T n -> Type :=
-  match n return tuple' _ n -> Type with
-  | 0 => fun T => f T
-  | S n' => fun Ts => (hlist' T n' f (fst Ts) * f (snd Ts))%type
-  end.
-Global Arguments hlist' {T n} f _.
-
-Definition hlist {T n} (f : T -> Type) : forall (Ts : tuple T n), Type :=
-  match n return tuple _ n -> Type with
-  | 0 => fun _ => unit
-  | S n' => @hlist' T n' f
-  end.
-
 Fixpoint to_list' {T} (n:nat) {struct n} : tuple' T n -> list T :=
   match n with
   | 0 => fun x => (x::nil)%list