diff --git a/_CoqProject b/_CoqProject
index 2793abada3d6f975a9c44ad72b8acceb0f90839c..570535e83fcc12e866c7efcd32e94598586c2e51 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -35,6 +35,7 @@ prelude/decidable.v
 prelude/list.v
 prelude/error.v
 prelude/functions.v
+prelude/hlist.v
 algebra/option.v
 algebra/cmra.v
 algebra/cmra_big_op.v
diff --git a/prelude/hlist.v b/prelude/hlist.v
new file mode 100644
index 0000000000000000000000000000000000000000..1f307b0628735395b6d069b0589528425f1c1002
--- /dev/null
+++ b/prelude/hlist.v
@@ -0,0 +1,18 @@
+From iris.prelude Require Import base.
+
+(* Not using [list Type] in order to avoid universe inconsistencies *)
+Inductive tlist := tnil : tlist | tcons : Type → tlist → tlist.
+
+Inductive hlist : tlist → Type :=
+  | hnil : hlist tnil
+  | hcons {A As} : A → hlist As → hlist (tcons A As).
+
+Fixpoint himpl (As : tlist) (B : Type) : Type :=
+  match As with tnil => B | tcons A As => A → himpl As B end.
+
+Definition happly {As B} (f : himpl As B) (xs : hlist As) : B :=
+  (fix go As xs :=
+    match xs in hlist As return himpl As B → B with
+    | hnil => λ f, f
+    | hcons A As x xs => λ f, go As xs (f x)
+    end) _ xs f.