diff --git a/_CoqProject b/_CoqProject
index d8f6edf734d3b3bbc0a8e3fe50ffad6105f4dd9b..53a3c0def87690092e9eabc775cf6a11b59fdd07 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -53,6 +53,7 @@ algebra/iprod.v
 algebra/upred.v
 algebra/upred_tactics.v
 algebra/upred_big_op.v
+algebra/upred_hlist.v
 algebra/frac.v
 algebra/csum.v
 algebra/list.v
diff --git a/algebra/upred_hlist.v b/algebra/upred_hlist.v
new file mode 100644
index 0000000000000000000000000000000000000000..ba779b5235c8f273317aae42ccb32d431b8c5dd9
--- /dev/null
+++ b/algebra/upred_hlist.v
@@ -0,0 +1,42 @@
+From iris.prelude Require Export hlist.
+From iris.algebra Require Export upred.
+Import uPred.
+
+Fixpoint uPred_hexist {M As} : himpl As (uPred M) → uPred M :=
+  match As return himpl As (uPred M) → uPred M with
+  | tnil => id
+  | tcons A As => λ Φ, ∃ x, uPred_hexist (Φ x)
+  end%I.
+Fixpoint uPred_hforall {M As} : himpl As (uPred M) → uPred M :=
+  match As return himpl As (uPred M) → uPred M with
+  | tnil => id
+  | tcons A As => λ Φ, ∀ x, uPred_hforall (Φ x)
+  end%I.
+
+Section hlist.
+Context {M : ucmraT}.
+
+Lemma hexist_exist {As B} (f : himpl As B) (Φ : B → uPred M) :
+  uPred_hexist (hcompose Φ f) ⊣⊢ ∃ xs : hlist As, Φ (f xs).
+Proof.
+  apply (anti_symm _).
+  - induction As as [|A As IH]; simpl.
+    + by rewrite -(exist_intro hnil) .
+    + apply exist_elim=> x; rewrite IH; apply exist_elim=> xs.
+      by rewrite -(exist_intro (hcons x xs)).
+  - apply exist_elim=> xs; induction xs as [|A As x xs IH]; simpl; auto.
+    by rewrite -(exist_intro x).
+Qed.
+
+Lemma hforall_forall {As B} (f : himpl As B) (Φ : B → uPred M) :
+  uPred_hforall (hcompose Φ f) ⊣⊢ ∀ xs : hlist As, Φ (f xs).
+Proof.
+  apply (anti_symm _).
+  - apply forall_intro=> xs; induction xs as [|A As x xs IH]; simpl; auto.
+    by rewrite (forall_elim x).
+  - induction As as [|A As IH]; simpl.
+    + by rewrite (forall_elim hnil) .
+    + apply forall_intro=> x; rewrite -IH; apply forall_intro=> xs.
+      by rewrite (forall_elim (hcons x xs)).
+Qed.
+End hlist.
diff --git a/prelude/hlist.v b/prelude/hlist.v
index 1f307b0628735395b6d069b0589528425f1c1002..7821ef94130f77a7d264264b07c58e12ac7bb0e8 100644
--- a/prelude/hlist.v
+++ b/prelude/hlist.v
@@ -16,3 +16,13 @@ Definition happly {As B} (f : himpl As B) (xs : hlist As) : B :=
     | hnil => λ f, f
     | hcons A As x xs => λ f, go As xs (f x)
     end) _ xs f.
+Coercion happly : himpl >-> Funclass.
+
+Fixpoint hcompose {As B C} (f : B → C) {struct As} : himpl As B → himpl As C :=
+  match As with
+  | tnil => f
+  | tcons A As => λ g x, hcompose f (g x)
+  end.
+
+Definition hinit {B} (y : B) : himpl tnil B := y.
+Definition hlam {A As B} (f : A → himpl As B) : himpl (tcons A As) B := f.
diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index 2b9436e8976a61e95b8691bed105476b353e37f1..b64ef1f0f1cdd86526535a72dc8dc6f2e543f7ac 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -895,8 +895,7 @@ Lemma tac_forall_intro {A} Δ (Φ : A → uPred M) : (∀ a, Δ ⊢ Φ a) → Δ
 Proof. apply forall_intro. Qed.
 
 Class ForallSpecialize {As} (xs : hlist As)
-    (P : uPred M) (Φ : himpl As (uPred M)) :=
-  forall_specialize : P ⊢ happly Φ xs.
+  (P : uPred M) (Φ : himpl As (uPred M)) := forall_specialize : P ⊢ Φ xs.
 Arguments forall_specialize {_} _ _ _ {_}.
 
 Global Instance forall_specialize_nil P : ForallSpecialize hnil P P | 100.
@@ -908,7 +907,7 @@ Proof. rewrite /ForallSpecialize /= => <-. by rewrite (forall_elim x). Qed.
 
 Lemma tac_forall_specialize {As} Δ Δ' i p P (Φ : himpl As (uPred M)) Q xs :
   envs_lookup i Δ = Some (p, P) → ForallSpecialize xs P Φ →
-  envs_simple_replace i p (Esnoc Enil i (happly Φ xs)) Δ = Some Δ' →
+  envs_simple_replace i p (Esnoc Enil i (Φ xs)) Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros. rewrite envs_simple_replace_sound //; simpl.