diff --git a/algebra/csum.v b/algebra/csum.v
index 9bc08217b15613ad7ca61327ec99451f0173ef87..5810079fd0b9d60efe345ca453a4c64fa4d61942 100644
--- a/algebra/csum.v
+++ b/algebra/csum.v
@@ -8,8 +8,8 @@ Local Arguments cmra_validN _ _ !_ /.
 Local Arguments cmra_valid _  !_ /.
 
 Inductive csum (A B : Type) :=
-| Cinl : A -> csum A B
-| Cinr : B -> csum A B
+| Cinl : A → csum A B
+| Cinr : B → csum A B
 | CsumBot : csum A B.
 Arguments Cinl {_ _} _.
 Arguments Cinr {_ _} _.
@@ -22,13 +22,13 @@ Implicit Types b : B.
 
 (* Cofe *)
 Inductive csum_equiv : Equiv (csum A B) :=
-  | Cinl_equiv a a' : a ≡ a' -> Cinl a ≡ Cinl a'
-  | Cinlr_equiv b b' : b ≡ b' -> Cinr b ≡ Cinr b'
+  | Cinl_equiv a a' : a ≡ a' → Cinl a ≡ Cinl a'
+  | Cinlr_equiv b b' : b ≡ b' → Cinr b ≡ Cinr b'
   | CsumBot_equiv : CsumBot ≡ CsumBot.
 Existing Instance csum_equiv.
 Inductive csum_dist : Dist (csum A B) :=
-  | Cinl_dist n a a' : a ≡{n}≡ a' -> Cinl a ≡{n}≡ Cinl a'
-  | Cinlr_dist n b b' : b ≡{n}≡ b' -> Cinr b ≡{n}≡ Cinr b'
+  | Cinl_dist n a a' : a ≡{n}≡ a' → Cinl a ≡{n}≡ Cinl a'
+  | Cinlr_dist n b b' : b ≡{n}≡ b' → Cinr b ≡{n}≡ Cinr b'
   | CsumBot_dist n : CsumBot ≡{n}≡ CsumBot.
 Existing Instance csum_dist.
 
diff --git a/algebra/upred_hlist.v b/algebra/upred_hlist.v
index ba779b5235c8f273317aae42ccb32d431b8c5dd9..82d0e55aac82cd436a93a94f29759fcb42ac0d00 100644
--- a/algebra/upred_hlist.v
+++ b/algebra/upred_hlist.v
@@ -25,7 +25,7 @@ Proof.
     + 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).
+    by rewrite -(exist_intro x) IH.
 Qed.
 
 Lemma hforall_forall {As B} (f : himpl As B) (Φ : B → uPred M) :
@@ -33,7 +33,7 @@ Lemma hforall_forall {As B} (f : himpl As B) (Φ : B → uPred M) :
 Proof.
   apply (anti_symm _).
   - apply forall_intro=> xs; induction xs as [|A As x xs IH]; simpl; auto.
-    by rewrite (forall_elim x).
+    by rewrite (forall_elim x) IH.
   - induction As as [|A As IH]; simpl.
     + by rewrite (forall_elim hnil) .
     + apply forall_intro=> x; rewrite -IH; apply forall_intro=> xs.
diff --git a/heap_lang/lib/spawn.v b/heap_lang/lib/spawn.v
index a380c8d8bf37d0bb1e490b1c0e59553dfbbd4be8..7ef95a18caf16265977ea8325fb7afdf9ca0ce5b 100644
--- a/heap_lang/lib/spawn.v
+++ b/heap_lang/lib/spawn.v
@@ -77,11 +77,11 @@ Proof.
   iLöb as "IH". wp_rec. wp_focus (! _)%E. iInv N as {v} "[Hl Hinv]".
   wp_load. iDestruct "Hinv" as "[%|Hinv]"; subst.
   - iSplitL "Hl"; [iNext; iExists _; iFrame; eauto|].
-    wp_case. wp_seq. iApply ("IH" with "Hγ Hv").
-  - iDestruct "Hinv" as {v'} "[% [HΨ|Hγ']]"; subst.
+    wp_match. iApply ("IH" with "Hγ Hv").
+  - iDestruct "Hinv" as {v'} "[% [HΨ|Hγ']]"; simplify_eq/=.
     + iSplitL "Hl Hγ".
       { iNext. iExists _; iFrame; eauto. }
-      wp_case. wp_let. iPvsIntro. by iApply "Hv".
+      wp_match. by iApply "Hv".
     + iCombine "Hγ" "Hγ'" as "Hγ". iDestruct (own_valid with "Hγ") as %[].
 Qed.
 End proof.
diff --git a/heap_lang/notation.v b/heap_lang/notation.v
index cf0c7db5c98facdcee53ffcea03c8b3012af9eee..0ebbc77e5189c290a93a4ff320116e1e7d953a35 100644
--- a/heap_lang/notation.v
+++ b/heap_lang/notation.v
@@ -99,3 +99,17 @@ Notation "'let:' x := e1 'in' e2" := (LamV x%bind e2%E e1%E)
   (at level 102, x at level 1, e1, e2 at level 200) : val_scope.
 Notation "e1 ;; e2" := (LamV BAnon e2%E e1%E)
   (at level 100, e2 at level 200, format "e1  ;;  e2") : val_scope.
+
+(** Notations for option *)
+Notation NONE := (InjL #()).
+Notation SOME x := (InjR x).
+
+Notation NONEV := (InjLV #()).
+Notation SOMEV x := (InjRV x).
+
+Notation "'match:' e0 'with' 'NONE' => e1 | 'SOME' x => e2 'end'" :=
+  (Match e0 BAnon e1 x%bind e2)
+  (e0, e1, x, e2 at level 200) : expr_scope.
+Notation "'match:' e0 'with' 'SOME' x => e2 | 'NONE' => e1 |  'end'" :=
+  (Match e0 BAnon e1 x%bind e2)
+  (e0, e1, x, e2 at level 200, only parsing) : expr_scope.
diff --git a/heap_lang/proofmode.v b/heap_lang/proofmode.v
index bd01b72a48afe156209c2d1dd0d4c1dc19ed08de..fa9b31fca7b5346f59c2d60d8c940df6a14dd92e 100644
--- a/heap_lang/proofmode.v
+++ b/heap_lang/proofmode.v
@@ -148,7 +148,7 @@ Tactic Notation "wp_store" :=
       |let l := match goal with |- _ = Some (_, (?l ↦{_} _)%I) => l end in
        iAssumptionCore || fail "wp_store: cannot find" l "↦ ?"
       |env_cbv; reflexivity
-      |wp_finish]
+      |wp_finish; try wp_seq]
   | _ => fail "wp_store: not a 'wp'"
   end.
 
diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index 2411087c3d92d5eaa58f74bca73b7eef1aaa91bf..4f42702a81d0f10a813216d5f0abd87b0b289aef 100644
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
@@ -92,16 +92,16 @@ Tactic Notation "wp_if" :=
   | _ => fail "wp_if: not a 'wp'"
   end.
 
-Tactic Notation "wp_case" :=
+Tactic Notation "wp_match" :=
   lazymatch goal with
   | |- _ ⊢ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval hnf in e' with
     | Case _ _ _ =>
       wp_bind K;
-      etrans; [|first[eapply wp_case_inl; wp_done|eapply wp_case_inr; wp_done]];
-      wp_finish
-    end) || fail "wp_case: cannot find 'Case' in" e
-  | _ => fail "wp_case: not a 'wp'"
+      etrans; [|first[eapply wp_match_inl; wp_done|eapply wp_match_inr; wp_done]];
+      simpl_subst; wp_finish
+    end) || fail "wp_match: cannot find 'Match' in" e
+  | _ => fail "wp_match: not a 'wp'"
   end.
 
 Tactic Notation "wp_focus" open_constr(efoc) :=
diff --git a/prelude/hlist.v b/prelude/hlist.v
index 7821ef94130f77a7d264264b07c58e12ac7bb0e8..8c888c732290a9b90917fe6d68b26ffc56ded8c1 100644
--- a/prelude/hlist.v
+++ b/prelude/hlist.v
@@ -1,4 +1,4 @@
-From iris.prelude Require Import base.
+From iris.prelude Require Import tactics.
 
 (* Not using [list Type] in order to avoid universe inconsistencies *)
 Inductive tlist := tnil : tlist | tcons : Type → tlist → tlist.
@@ -7,22 +7,53 @@ Inductive hlist : tlist → Type :=
   | hnil : hlist tnil
   | hcons {A As} : A → hlist As → hlist (tcons A As).
 
+Fixpoint tapp (As Bs : tlist) : tlist :=
+  match As with tnil => Bs | tcons A As => tcons A (tapp As Bs) end.
+Fixpoint happ {As Bs} (xs : hlist As) (ys : hlist Bs) : hlist (tapp As Bs) :=
+  match xs with hnil => ys | hcons _ _ x xs => hcons x (happ xs ys) end.
+
+Fixpoint hhead {A As} (xs : hlist (tcons A As)) : A :=
+  match xs with hnil => () | hcons _ _ x _ => x end.
+Fixpoint htail {A As} (xs : hlist (tcons A As)) : hlist As :=
+  match xs with hnil => () | hcons _ _ _ xs => xs end.
+
+Fixpoint hheads {As Bs} : hlist (tapp As Bs) → hlist As :=
+  match As with
+  | tnil => λ _, hnil
+  | tcons A As => λ xs, hcons (hhead xs) (hheads (htail xs))
+  end.
+Fixpoint htails {As Bs} : hlist (tapp As Bs) → hlist Bs :=
+  match As with
+  | tnil => id
+  | tcons A As => λ xs, htails (htail xs)
+  end.
+
 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 :=
+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.
+Arguments hlam _ _ _ _ _/.
+
+Definition hcurry {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.
-Coercion happly : himpl >-> Funclass.
+Coercion hcurry : himpl >-> Funclass.
+
+Fixpoint huncurry {As B} : (hlist As → B) → himpl As B :=
+  match As with
+  | tnil => λ f, f hnil
+  | tcons x xs => λ f, hlam (λ x, huncurry (f ∘ hcons x))
+  end.
+
+Lemma hcurry_uncurry {As B} (f : hlist As → B) xs : huncurry f xs = f xs.
+Proof. by induction xs as [|A As x xs IH]; simpl; rewrite ?IH. Qed.
 
 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)
+  | tcons A As => λ g, hlam (λ 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/tactics.v b/proofmode/tactics.v
index 882c35f4ce5f9b26d00ccb46fb25482e1c3df149..eff7af382973b12fadaead33c687445a1ba6a5d9 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -11,7 +11,6 @@ Declare Reduction env_cbv := cbv [
   bool_eq_dec bool_rec bool_rect bool_dec eqb andb (* bool *)
   assci_eq_dec ascii_to_digits Ascii.ascii_dec Ascii.ascii_rec Ascii.ascii_rect
   string_eq_dec string_rec string_rect (* strings *)
-  himpl happly
   env_persistent env_spatial envs_persistent
   envs_lookup envs_lookup_delete envs_delete envs_app
     envs_simple_replace envs_replace envs_split envs_clear_spatial].
@@ -35,6 +34,11 @@ Tactic Notation "iTypeOf" constr(H) tactic(tac):=
   | Some (?p,?P) => tac p P
   end.
 
+Ltac iMatchGoal tac :=
+  match goal with
+  | |- context[ environments.Esnoc _ ?x ?P ] => tac x P
+  end.
+
 (** * Start a proof *)
 Tactic Notation "iProof" :=
   lazymatch goal with
@@ -135,7 +139,7 @@ Local Tactic Notation "iSpecializeArgs" constr(H) open_constr(xs) :=
     eapply tac_forall_specialize with _ H _ _ _ xs; (* (i:=H) (a:=x) *)
       [env_cbv; reflexivity || fail 1 "iSpecialize:" H "not found"
       |apply _ || fail 1 "iSpecialize:" H "not a forall of the right arity or type"
-      |env_cbv; reflexivity|]
+      |cbn [himpl hcurry]; reflexivity|]
   end.
 
 Local Tactic Notation "iSpecializePat" constr(H) constr(pat) :=
@@ -790,6 +794,10 @@ Tactic Notation "iRewrite" open_constr(t) "in" constr(H) :=
 Tactic Notation "iRewrite" "-" open_constr(t) "in" constr(H) :=
   iRewriteCore true t in H.
 
+Ltac iSimplifyEq := repeat (
+  iMatchGoal ltac:(fun H P => match P with (_ = _)%I => iDestruct H as %? end)
+  || simplify_eq/=).
+
 (* Make sure that by and done solve trivial things in proof mode *)
 Hint Extern 0 (of_envs _ ⊢ _) => by iPureIntro.
 Hint Extern 0 (of_envs _ ⊢ _) => iAssumption.
diff --git a/tests/barrier_client.v b/tests/barrier_client.v
index 7665f27c63066f69a1c1a3fc54a0afecf47f697e..4d17d5a920579e396c306fb257f0ced2ac34fdaa 100644
--- a/tests/barrier_client.v
+++ b/tests/barrier_client.v
@@ -45,7 +45,7 @@ Section client.
     iApply (wp_par heapN N (λ _, True%I) (λ _, True%I)); first done.
     iFrame "Hh". iSplitL "Hy Hs".
     - (* The original thread, the sender. *)
-      wp_store. wp_seq. iApply signal_spec; iFrame "Hs"; iSplit; [|done].
+      wp_store. iApply signal_spec; iFrame "Hs"; iSplit; [|done].
       iExists _; iSplitL; [done|]. iAlways; iIntros {n}. wp_let. by wp_op.
     - (* The two spawned threads, the waiters. *)
       iSplitL; [|by iIntros {_ _} "_ >"].
diff --git a/tests/heap_lang.v b/tests/heap_lang.v
index 84aa55224e86ba09384dc797cb0362fd38e0d478..61f35795800d3af3edfa4200a8ad71090238b7b5 100644
--- a/tests/heap_lang.v
+++ b/tests/heap_lang.v
@@ -27,7 +27,7 @@ Section LiftingTests.
      nclose N ⊆ E → heap_ctx N ⊢ WP heap_e @ E {{ v, v = #2 }}.
   Proof.
     iIntros {HN} "#?". rewrite /heap_e. iApply (wp_mask_weaken N); first done.
-    wp_alloc l. wp_let. wp_load. wp_op. wp_store. wp_seq. by wp_load.
+    wp_alloc l. wp_let. wp_load. wp_op. wp_store. by wp_load.
   Qed.
 
   Definition heap_e2  : expr [] :=
@@ -39,7 +39,7 @@ Section LiftingTests.
   Proof.
     iIntros {HN} "#?". rewrite /heap_e2. iApply (wp_mask_weaken N); first done.
     wp_alloc l. wp_let. wp_alloc l'. wp_let.
-    wp_load. wp_op. wp_store. wp_seq. wp_load. done.
+    wp_load. wp_op. wp_store. wp_load. done.
   Qed.
 
   Definition FindPred : val :=
diff --git a/tests/one_shot.v b/tests/one_shot.v
index a7b267d76d1c50f44a7830f2a5b173c7a21e90b3..e1b70e06a213b1e73f2abaebb6d05502442d5c5a 100644
--- a/tests/one_shot.v
+++ b/tests/one_shot.v
@@ -71,15 +71,15 @@ Proof.
       + iSplit. iRight; iExists m; by iSplitL "Hl". eauto. }
     wp_let. iPvsIntro. iIntros "!". wp_seq.
     iDestruct "Hv" as "[%|Hv]"; last iDestruct "Hv" as {m} "[% Hγ']"; subst.
-    { wp_case. wp_seq. by iPvsIntro. }
-    wp_case. wp_let. wp_focus (! _)%E.
+    { wp_match. by iPvsIntro. }
+    wp_match. wp_focus (! _)%E.
     iInv> N as "[[Hl Hγ]|Hinv]"; last iDestruct "Hinv" as {m'} "[Hl Hγ]".
     { iCombine "Hγ" "Hγ'" as "Hγ". by iDestruct (own_valid with "Hγ") as "%". }
     wp_load.
     iCombine "Hγ" "Hγ'" as "Hγ".
     iDestruct (own_valid with "#Hγ") as %[=->]%dec_agree_op_inv.
     iSplitL "Hl"; [iRight; by eauto|].
-    wp_case. wp_let. iApply wp_assert'. wp_op=>?; simplify_eq/=; eauto.
+    wp_match. iApply wp_assert'. wp_op=>?; simplify_eq/=; eauto.
 Qed.
 
 Lemma hoare_one_shot (Φ : val → iProp) :
diff --git a/tests/tree_sum.v b/tests/tree_sum.v
index eef5211bec5c51197377f8e2763cc28d1c2e3d13..b96686ebd14417433a959d3c25b50f0e8e5e6017 100644
--- a/tests/tree_sum.v
+++ b/tests/tree_sum.v
@@ -40,13 +40,13 @@ Lemma sum_loop_wp `{!heapG Σ} heapN v t l (n : Z) (Φ : val → iPropG heap_lan
   ⊢ WP sum_loop v #l {{ Φ }}.
 Proof.
   iIntros "(#Hh & Hl & Ht & HΦ)".
-  iLöb {v t l n Φ} as "IH". wp_rec. wp_let.
+  iLöb {v t l n Φ} as "IH". wp_rec; wp_let.
   destruct t as [n'|tl tr]; simpl in *.
   - iDestruct "Ht" as "%"; subst.
-    wp_case. wp_let. wp_load. wp_op. wp_store.
+    wp_match. wp_load. wp_op. wp_store.
     by iApply ("HΦ" with "Hl").
   - iDestruct "Ht" as {ll lr vl vr} "(% & Hll & Htl & Hlr & Htr)"; subst.
-    wp_case. wp_let. wp_proj. wp_load.
+    wp_match. wp_proj. wp_load.
     wp_apply ("IH" with "Hl Htl"). iIntros "Hl Htl".
     wp_seq. wp_proj. wp_load.
     wp_apply ("IH" with "Hl Htr"). iIntros "Hl Htr".