diff --git a/src/examples/gmap_option.v b/src/examples/gmap_option.v
index 6f8dd48..9e2aa95 100644
--- a/src/examples/gmap_option.v
+++ b/src/examples/gmap_option.v
@@ -29,13 +29,13 @@ Definition gmap_mov (a b: gmap K (option V)) : Prop :=
 Lemma gmap_dot_comm x y
   : gmap_dot x y = gmap_dot y x.
 Proof.
-intros. unfold gmap_dot, gmerge. apply map_eq. intro. rewrite lookup_merge.
+intros. unfold gmap_dot, gmerge. apply map_eq. intro i. rewrite lookup_merge.
     rewrite lookup_merge. unfold diag_None. destruct (x !! i), (y !! i); trivial.
 Qed.
   
 Lemma gmap_dot_assoc x y z
   : gmap_dot x (gmap_dot y z) = gmap_dot (gmap_dot x y) z.
-Proof. intros. unfold gmap_dot, gmerge. apply map_eq. intro. rewrite lookup_merge.
+Proof. intros. unfold gmap_dot, gmerge. apply map_eq. intro i. rewrite lookup_merge.
     rewrite lookup_merge.
     rewrite lookup_merge.
     unfold diag_None.
@@ -47,22 +47,22 @@ Qed.
 Lemma gmap_dot_empty
   : ∀ x : gmap K (option V), gmap_dot x ∅ = x.
 Proof.
-intros. unfold gmap_dot. apply map_eq. intro. rewrite lookup_merge. rewrite lookup_empty.
+intros x. unfold gmap_dot. apply map_eq. intro i. rewrite lookup_merge. rewrite lookup_empty.
     unfold diag_None, gmerge. destruct (x !! i); trivial.
 Qed.
 
 Lemma gmap_dot_empty_left
   : ∀ x : gmap K (option V), gmap_dot ∅ x = x.
 Proof.
-intros. unfold gmap_dot. apply map_eq. intro. rewrite lookup_merge. rewrite lookup_empty.
+intros x. unfold gmap_dot. apply map_eq. intro i. rewrite lookup_merge. rewrite lookup_empty.
     unfold diag_None, gmerge. destruct (x !! i); trivial.
 Qed.
 
 Lemma lookup_gmap_dot_left a b k
   : gmap_valid (gmap_dot a b) -> (a !! k ≠ None) -> (gmap_dot a b) !! k = a !! k.
 Proof.
-  unfold gmap_valid, gmap_dot. intros.
-  have j := H k. rewrite lookup_merge.
+  unfold gmap_valid, gmap_dot. intros Q R.
+  have j := Q k. rewrite lookup_merge.
   rewrite lookup_merge in j. unfold diag_None, gmerge in *. destruct (a !! k), (b !! k);
   trivial; contradiction.
 Qed.
@@ -70,7 +70,7 @@ Qed.
 Lemma lookup_gmap_dot_right a b k
   : gmap_valid (gmap_dot a b) -> (b !! k ≠ None) -> (gmap_dot a b) !! k = b !! k.
 Proof.
-  unfold gmap_valid, gmap_dot. intros. have j := H k. rewrite lookup_merge.
+  unfold gmap_valid, gmap_dot. intros Q R. have j := Q k. rewrite lookup_merge.
   rewrite lookup_merge in j. unfold diag_None, gmerge in *. destruct (a !! k), (b !! k);
   trivial; contradiction.
 Qed.
@@ -79,9 +79,9 @@ Lemma lookup_gmap_dot_3mid a b c k
   : gmap_valid (gmap_dot (gmap_dot a b) c) -> (b !! k ≠ None) ->
       gmap_dot (gmap_dot a b) c !! k = b !! k.
 Proof.
-  intros.
-  rewrite gmap_dot_comm in H.
-  rewrite gmap_dot_assoc in H.
+  intros Q R.
+  rewrite gmap_dot_comm in Q.
+  rewrite gmap_dot_assoc in Q.
   rewrite gmap_dot_comm.
   rewrite gmap_dot_assoc.
   apply lookup_gmap_dot_right; trivial.
@@ -91,8 +91,8 @@ Lemma lookup_gmap_dot_3left a b c k
   : gmap_valid (gmap_dot (gmap_dot a b) c) -> (a !! k ≠ None) ->
       gmap_dot (gmap_dot a b) c !! k = a !! k.
 Proof.
-  intros.
-  rewrite <- gmap_dot_assoc in H.
+  intros Q R.
+  rewrite <- gmap_dot_assoc in Q.
   rewrite <- gmap_dot_assoc.
   apply lookup_gmap_dot_left; trivial.
 Qed.
@@ -107,8 +107,8 @@ Qed.
 Lemma gmap_valid_left
   : ∀ x y : gmap K (option V), gmap_valid (gmap_dot x y) → gmap_valid x.
 Proof.
-  intros. unfold gmap_valid, gmap_dot in *.
-    intro. have h := H k. clear H. rewrite lookup_merge in h. unfold diag_None in h.
+  intros x y. unfold gmap_valid, gmap_dot in *.
+    intros Q k. have h := Q k. clear Q. rewrite lookup_merge in h. unfold diag_None in h.
         unfold gmerge in h.
         destruct (x !! k); trivial.
         destruct (y !! k); trivial. contradiction.
@@ -124,8 +124,8 @@ Lemma gmap_valid_update_singleton j x y (m: gmap K (option V)) :
   gmap_valid (gmap_dot {[j := Some x]} m) ->
   gmap_valid (gmap_dot {[j := Some y]} m).
 Proof.
-  intros. unfold gmap_valid, gmap_dot in *. intro.
-  have r := H k. rewrite lookup_merge. rewrite lookup_merge in r.
+  intros Q. unfold gmap_valid, gmap_dot in *. intro k.
+  have r := Q k. rewrite lookup_merge. rewrite lookup_merge in r.
   unfold gmerge, diag_None in *.
   have h : Decision (j = k) by solve_decision. destruct h.
   - subst k. rewrite lookup_singleton. rewrite lookup_singleton in r.
@@ -134,30 +134,6 @@ Proof.
     rewrite lookup_singleton_ne in r; trivial.
 Qed.
  
- (*
-#[refine]
-Global Instance gmap_tpcm : TPCM (gmap K (option V)) := {
-  m_valid p := gmap_valid p ;
-  dot a b := gmap_dot a b ;
-  mov a b := gmap_mov a b ;
-  unit := empty ;
-}.
- - apply gmap_valid_left.
- - unfold gmap_valid. intros. rewrite lookup_empty. trivial.
- - apply gmap_dot_empty.
- - intros. apply gmap_dot_comm.
- - intros. apply gmap_dot_assoc.
-  - intros. unfold gmap_mov. intro. trivial.
-  - intros. unfold gmap_mov in *. intros. apply H0. apply H. trivial.
-  - intros. split.
-    * unfold gmap_mov in H. apply H. apply H0.
-    * unfold gmap_mov in H. unfold gmap_mov. intro.
-        rewrite <- gmap_dot_assoc.
-        rewrite <- gmap_dot_assoc.
-        apply H.
-Defined.
-*)
-
 Definition gmap_le (a b : gmap K (option V)) := ∃ c , gmap_dot a c = b.
 
 Lemma le_of_subset (a b : gmap K (option V))
@@ -166,19 +142,19 @@ Proof.
   assert (∀ x : K * option V, Decision (match x with (k,v) => a !! k = None end)) as X
     by solve_decision.
   exists (map_filter (λ x , match x with (k,v) => a !! k = None end) X b).
-  unfold gmap_dot. apply map_eq. intro.
+  unfold gmap_dot. apply map_eq. intro i.
   have ff := f i.
   rewrite lookup_merge. unfold diag_None, gmerge. 
-  destruct (a !! i) eqn:ai.
+  destruct (a !! i) as [o|] eqn:ai.
   - rewrite map_lookup_filter.
-    unfold "≫=", option_bind. destruct (b!!i) eqn:bi.
-    + unfold guard. have fff := ff o. intuition. inversion H.
+    unfold "≫=", option_bind. destruct (b!!i) as [o0|] eqn:bi.
+    + unfold guard. have fff := ff o. have ffff := fff eq_refl. inversion ffff. subst o0.
       destruct (X (i, o)) as [e|e].
       * rewrite e in ai. discriminate.
       * trivial.
     + have fff := ff o. intuition.
   - rewrite map_lookup_filter.
-    unfold "≫=", option_bind. destruct (b!!i) eqn:bi; trivial.
+    unfold "≫=", option_bind. destruct (b!!i) as [o|] eqn:bi; trivial.
     destruct (X (i, o)); trivial.
     contradiction.
 Qed.
@@ -194,7 +170,7 @@ Lemma conjunct_and_gmap
 Proof.
   apply le_of_subset. intros k v e1.
   unfold gmap_dot in e1. rewrite lookup_merge in e1. unfold diag_None in e1.
-  destruct (a1 !! k) eqn:a1k; destruct (a2 !! k) eqn:a2k.
+  destruct (a1 !! k) as [o|] eqn:a1k; destruct (a2 !! k) as [o0|] eqn:a2k.
   - have l := a_disj _ _ _ a1k a2k. contradiction.
   - unfold gmerge in e1. inversion e1. subst o. unfold gmap_le in la1.
       destruct la1 as [d la]. subst c.
@@ -204,7 +180,7 @@ Proof.
       have gvk := gv k.
       rewrite lookup_merge in gvk. rewrite a1k in gvk. unfold diag_None in gvk.
       unfold gmerge. unfold gmerge in gvk. destruct (d !! k); trivial. contradiction.
-  - unfold gmerge in e1. inversion e1. subst o. unfold gmap_le in la2.
+  - unfold gmerge in e1. inversion e1. subst o0. unfold gmap_le in la2.
       destruct la2 as [d la]. subst c.
       unfold gmap_dot.
       unfold gmap_valid in gv. unfold gmap_dot in gv.
diff --git a/src/examples/hash_table_raw.v b/src/examples/hash_table_raw.v
index 772bcf8..5ebd031 100644
--- a/src/examples/hash_table_raw.v
+++ b/src/examples/hash_table_raw.v
@@ -88,7 +88,7 @@ Definition m (k: Key) (v: option Value) :=
 Lemma ht_valid_QueryFound j k v v0
   : V (ht_dot (s j (Some (k, v0))) (m k v)) -> v = Some v0.
 Proof.
-  unfold V, s, m. intros [z H]. destruct z. unfold ht_dot in *. unfold P in *.
+  unfold V, s, m. intros [z H]. destruct z as [ms slots]. unfold ht_dot in *. unfold P in *.
   repeat (rewrite gmap_dot_empty in H).
   repeat (rewrite gmap_dot_empty_left in H).
   destruct H as [H [H0 [H1 [H2 [H3 H4]]]]].
@@ -122,7 +122,7 @@ Lemma ht_valid_QueryReachedEnd k a v
   (is_full: full a k (hash k) ht_fixed_size)
   : V (ht_dot a (m k v)) -> v = None.
 Proof.
-  unfold V, s, m. intros [z H]. destruct z, a. unfold ht_dot in *. unfold P in *.
+  unfold V, s, m. intros [z H]. destruct z as [ms slots], a as [ms0 slots0]. unfold ht_dot in *. unfold P in *.
   unfold full in is_full.
   destruct H as [H [H0 [H1 [H2 [H3 H4]]]]].
   destruct is_full as [H5 [H6 [H7 H8]]].
@@ -139,7 +139,7 @@ Proof.
   repeat (rewrite gmap_dot_empty_left in H3).
   repeat (rewrite gmap_dot_empty in H4).
   repeat (rewrite gmap_dot_empty_left in H4).
-  destruct v; trivial. exfalso.
+  destruct v as [v|]; trivial. exfalso.
   have h := H3 k v.
   assert (gmap_dot {[k := Some (Some v)]} ms !! k = Some (Some (Some v))) as Q.
   {
@@ -167,7 +167,7 @@ Lemma ht_valid_QueryNotFound k a v j
   (is_full: full a k (hash k) j)
   : V (ht_dot (ht_dot a (m k v)) (s j None)) -> v = None.
 Proof.
-  unfold V, s, m. intros [z H]. destruct z, a. unfold ht_dot in *. unfold P in *.
+  unfold V, s, m. intros [z H]. destruct z as [ms slots], a as [ms0 slots0]. unfold ht_dot in *. unfold P in *.
   unfold full in is_full.
   destruct H as [H [H0 [H1 [H2 [H3 H4]]]]].
   destruct is_full as [H5 [H6 [H7 H8]]].
@@ -184,7 +184,7 @@ Proof.
   repeat (rewrite gmap_dot_empty_left in H3).
   repeat (rewrite gmap_dot_empty in H4).
   repeat (rewrite gmap_dot_empty_left in H4).
-  destruct v; trivial. exfalso.
+  destruct v as [v|]; trivial. exfalso.
   have h := H3 k v.
   assert (gmap_dot {[k := Some (Some v)]} ms !! k = Some (Some (Some v))) as Q.
   {
@@ -200,8 +200,8 @@ Proof.
   assert (i < j) as ihfs.
   {
     have hij : Decision (i < j) by solve_decision. destruct hij; trivial.
-    assert (j ≤ i) by lia.
-    have mm := H10 j H5 H11. destruct mm as [k1 [v1 mm]].
+    assert (j ≤ i) as Hle by lia.
+    have mm := H10 j H5 Hle. destruct mm as [k1 [v1 mm]].
     rewrite lookup_gmap_dot_3mid in mm.
     - rewrite lookup_singleton in mm. inversion mm.
     - trivial.
@@ -220,19 +220,19 @@ Lemma preserves_lt_fixed_size j a b slots
   : ∀ (i : nat) (e : option (option (Key * Value))),
     gmap_dot {[j := Some b]} slots !! i = Some e → i < ht_fixed_size.
 Proof.
-  intros.
+  intros i e Heq.
   (*have h : Decision (i = j) by solve_decision. destruct h.*)
-  destruct (gmap_dot {[j := Some a]} slots !! i) eqn:gd.
+  destruct (gmap_dot {[j := Some a]} slots !! i) as [o|] eqn:gd.
   - exact (ltfs i o gd).
-  - exfalso. unfold gmap_dot in H, gd.
-      rewrite lookup_merge in H.
+  - exfalso. unfold gmap_dot in Heq, gd.
+      rewrite lookup_merge in Heq.
       rewrite lookup_merge in gd.
       unfold diag_None, gmerge in *.
       have h : Decision (j = i) by solve_decision. destruct h.
       + subst j.
-        rewrite lookup_singleton in H.
+        rewrite lookup_singleton in Heq.
         rewrite lookup_singleton in gd. destruct (slots !! i); discriminate.
-      + rewrite lookup_singleton_ne in H; trivial.
+      + rewrite lookup_singleton_ne in Heq; trivial.
         rewrite lookup_singleton_ne in gd; trivial.
         destruct (slots !! i); discriminate.
 Qed.
@@ -296,8 +296,7 @@ Lemma preserves_unique_keys j k v v1 slots
     ∧ gmap_dot {[j := Some (Some (k, v))]} slots !! i2 = Some (Some (Some (k0, v3)))
     → i1 = i2.
 Proof.
-  intros.
-  destruct H as [H H0].
+  intros i1 i2 k0 v2 v3 [H H0].
   have ed : Decision (i1 = j) by solve_decision. destruct ed.
     - have ed : Decision (i2 = j) by solve_decision. destruct ed.
       + subst. trivial.
@@ -344,8 +343,8 @@ Proof.
     rewrite lookup_singleton in ac.
     destruct (slots !! j), (slots0 !! j); discriminate.
   - rewrite lookup_singleton_ne in ac; trivial.
-    destruct (slots !! i2), (slots0 !! i2); try inversion ac; try discriminate.
-    + subst o. inversion zz. inversion zz. subst k. contradiction.
+    destruct (slots !! i2) as [a1|], (slots0 !! i2) as [b1|]; try inversion ac; try discriminate.
+    + subst b1. inversion zz. inversion zz. subst k. contradiction.
 Qed.
 
 Lemma pukn_helper j k0 k v v1 slots v0 ms ms0 slots0 i2 v2
diff --git a/src/guarding/internal/auth_frag_util.v b/src/guarding/internal/auth_frag_util.v
index 40ed8e7..399f48e 100644
--- a/src/guarding/internal/auth_frag_util.v
+++ b/src/guarding/internal/auth_frag_util.v
@@ -1,9 +1,7 @@
+From iris.prelude Require Import options.
 From iris.algebra Require Export cmra updates.
 From iris.algebra Require Import proofmode_classes.
 From iris.algebra Require Import auth.
-From iris.algebra Require Import functions.
-From iris.algebra Require Import gmap.
-From iris.prelude Require Import options.
 
 From iris.base_logic Require Import upred.
 From iris.base_logic.lib Require Export own iprop.
@@ -12,8 +10,6 @@ From iris.proofmode Require Import ltac_tactics.
 From iris.proofmode Require Import tactics.
 From iris.proofmode Require Import coq_tactics.
 
-From stdpp Require Import numbers.
-
 Require Import guarding.own_and.
 
 Section AuthFragUtil.
@@ -25,9 +21,9 @@ Context `{Disc : CmraDiscrete C}.
 
 Lemma auth_op_rhs_is_frag (p: C) z (val : ✓ (● p ⋅ z)) : ∃ q , z = ◯ q.
 Proof.
-  destruct z. exists view_frag_proj. rename view_frag_proj into f.
+  destruct z as [a f]. exists f.
   unfold "◯", "◯V". f_equal.
-  destruct view_auth_proj; trivial.
+  destruct a as [p0|]; trivial.
   exfalso.
   unfold "●", "●V" in val.
   
@@ -42,7 +38,7 @@ Proof.
   
   rewrite /op /view_op_instance /view_auth_proj /view_frag_proj in val2.
   rewrite /valid /view_valid_instance /view_auth_proj in val2.
-  destruct p0.
+  destruct p0 as [d a].
   assert (Some (DfracOwn 1, to_agree p) ⋅ Some (d, a)
       = Some (DfracOwn 1 ⋅ d, to_agree p ⋅ a)) as Q.
     { trivial. }
@@ -66,8 +62,8 @@ Lemma rhs_has_auth (x y : C) (q1 q2: auth C)
 Proof.
   have ao := auth_op_rhs_is_frag x q1 v.
   destruct ao as [q ao]. subst q1.
-  destruct q2.
-  exists (◯ view_frag_proj).
+  destruct q2 as [a f].
+  exists (◯ f).
   unfold "●", "●V", "◯", "◯V".
   
   rewrite view_op_rw.
@@ -78,10 +74,10 @@ Proof.
     rewrite view_op_rw in eq.
     rewrite view_op_rw in eq.
     
-    inversion eq.
-    unfold view.view_auth_proj in H.
-    setoid_rewrite H.
-    + destruct view_auth_proj; trivial.
+    inversion eq as [Q R].
+    unfold view.view_auth_proj in Q.
+    setoid_rewrite Q.
+    + destruct a; trivial.
   - rewrite left_id. trivial.
 Qed.
   
@@ -258,11 +254,7 @@ Qed.
 Lemma auth_frag_disjointness_helper (q r : C) (a b : auth C)
   (eq1 : ◯ q ⋅ a ≡ ● r ⋅ b) : ◯ q ≼ b.
 Proof.
-  destruct a, b.
-  rename view_frag_proj into f.
-  rename view_auth_proj into g.
-  rename view_frag_proj0 into f0.
-  rename view_auth_proj0 into g0.
+  destruct a as [g f], b as [g0 f0].
   unfold "◯", "◯V" in eq1.
   unfold "●", "●V" in eq1.
   unfold "◯", "◯V".
@@ -273,9 +265,9 @@ Proof.
   replace (@View C C (@auth_view_rel C) (Some (DfracOwn 1, to_agree r)) ε ⋅ @View C C (@auth_view_rel C) g0 f0)
     with (@View C C (@auth_view_rel C) (Some (DfracOwn 1, to_agree r) ⋅ g0) (ε ⋅ f0)) in eq1 by trivial.
     
-  inversion eq1.
-  unfold view_frag_proj in H0.
-  generalize H0.
+  inversion eq1 as [Q R].
+  unfold view_frag_proj in R.
+  generalize R.
   rewrite ucmra_unit_left_id.
   intro X.
   
diff --git a/src/guarding/internal/wsat_util.v b/src/guarding/internal/wsat_util.v
index 742f61b..31c484d 100644
--- a/src/guarding/internal/wsat_util.v
+++ b/src/guarding/internal/wsat_util.v
@@ -1,10 +1,9 @@
-From stdpp Require Export coPset.
+From iris.prelude Require Import options.
 From iris.algebra Require Import gmap_view gset coPset.
 From iris.proofmode Require Import proofmode.
-From iris.base_logic.lib Require Export own.
-From iris.base_logic.lib Require Export wsat.
-From iris.prelude Require Import options.
+From iris.base_logic.lib Require Export own wsat.
 Import uPred.
+From stdpp Require Export coPset.
 From iris.algebra Require Import functions.
 
 Section wsat_util.
@@ -212,7 +211,7 @@ Lemma own_updateP_extra `{i : !inG Σ A} `{j : !inG Σ B} (P : A → gname → P
     (∀ (n : nat) (mz : option A) (N : gname → Prop) , ✓{n} (a ⋅? mz) → pred_finite N → ∃ (y: A) (γ': gname), P y γ' ∧ ✓{n} (y ⋅? mz) ∧ ¬ N γ') →
     (✓ b) →
     own γ a ⊢ |==> ∃ a' γ', ⌜P a' γ'⌝ ∗ own γ a' ∗ own γ' b.
-Proof using H Σ.
+Proof.
   intros Hupd Hvalb. rewrite !own.own_eq.
   rewrite -(bupd_mono (∃ m,
     ⌜ ∃ a' γ', m = (own.iRes_singleton γ a' ⋅ own.iRes_singleton γ' b) ∧ P a' γ' ⌝ ∧ uPred_ownM m)%I).
diff --git a/src/guarding/own_and.v b/src/guarding/own_and.v
index 2b539de..f57041c 100644
--- a/src/guarding/own_and.v
+++ b/src/guarding/own_and.v
@@ -66,13 +66,13 @@ Section ConjunctOwnRule2.
     (project (x ⋅ y) γ : option A) ≡{n}≡ (project x γ ⋅ project y γ).
   Proof.
     unfold project. rewrite lookup_op.
-    destruct (x (inG_id i) !! γ) eqn:p1; destruct (y (inG_id i) !! γ) eqn:p2.
+    destruct (x (inG_id i) !! γ) as [o|] eqn:p1; destruct (y (inG_id i) !! γ) as [o0|] eqn:p2.
     - rewrite p1. rewrite p2.
         replace (Some o ⋅ Some o0) with (Some (o ⋅ o0)) by trivial.
         enough (cmra_transport (eq_sym inG_prf) (own.inG_fold (o ⋅ o0)) ≡{n}≡ 
                 cmra_transport (eq_sym inG_prf) (own.inG_fold o)
-                ⋅ cmra_transport (eq_sym inG_prf) (own.inG_fold o0)).
-        { intros. setoid_rewrite H. trivial. }
+                ⋅ cmra_transport (eq_sym inG_prf) (own.inG_fold o0)) as Hcmeq.
+        { intros. setoid_rewrite Hcmeq. trivial. }
         setoid_rewrite <- cmra_transport_op.
         f_equiv.
         unfold own.inG_fold. apply equiv_dist.
@@ -88,8 +88,8 @@ Section ConjunctOwnRule2.
     unfold Proper, "==>". intros x y H γ γ0 s0. unfold project. subst γ0.
     assert (x (inG_id i) !! γ ≡{n}≡ y (inG_id i) !! γ) as M.
     { enough (x (inG_id i) ≡{n}≡ y (inG_id i)). { trivial. } trivial. }
-    destruct (x (inG_id i) !! γ);
-    destruct (y (inG_id i) !! γ).
+    destruct (x (inG_id i) !! γ) as [o|];
+    destruct (y (inG_id i) !! γ) as [o0|].
     - assert (o ≡{n}≡ o0) as Q.
       + unfold "≡" in M. unfold ofe_equiv, optionO, option_equiv in M.
             inversion M. trivial.
@@ -122,7 +122,7 @@ Section ConjunctOwnRule2.
   Proof.
     intro p.
     unfold project in p.
-    destruct (z (inG_id i) !! γ) eqn:e.
+    destruct (z (inG_id i) !! γ) as [o|] eqn:e.
     - assert ((cmra_transport (eq_sym inG_prf) (own.inG_fold o)) ≡ z') as X.
       { unfold "≡", ofe_equiv, optionO, option_equiv in p. inversion p. trivial. }
       unfold includedN.
@@ -264,7 +264,7 @@ Section ConjunctOwnRule2Ucmra.
     @uPred_cmra_incl Σ (option A) (Some x) (Some y)  ⊢ ⌜ x ≼ y ⌝.
   Proof.
     unfold uPred_cmra_incl. iIntros "eq". iDestruct "eq" as (c) "eq".
-    iDestruct (discrete_eq_1 with "eq") as "%eq". unfold "≼". iPureIntro. destruct c.
+    iDestruct (discrete_eq_1 with "eq") as "%eq". unfold "≼". iPureIntro. destruct c as [c|].
     - exists c. setoid_rewrite <- Some_op in eq. inversion eq. trivial.
     - exists ε. rewrite right_id. inversion eq. trivial.
   Qed.
diff --git a/src/guarding/own_and_own_sep.v b/src/guarding/own_and_own_sep.v
index 565b83e..af9e536 100644
--- a/src/guarding/own_and_own_sep.v
+++ b/src/guarding/own_and_own_sep.v
@@ -29,7 +29,7 @@ Lemma valid_project (x: iResUR Σ) (γ: gname) (n: nat) :
 Proof.
   intros.
   unfold project.
-  destruct (x (inG_id i) !! γ) eqn:p.
+  destruct (x (inG_id i) !! γ) as [o|] eqn:p.
   - apply cmra_transport_validN.
     rewrite <- own.inG_unfold_validN.
     setoid_rewrite own.inG_unfold_fold.
@@ -43,14 +43,14 @@ Qed.
 
 Lemma some_op_equiv (a b c : A)
   : a ≡ b ⋅ c -> Some a ≡ Some b ⋅ Some c.
-Proof. intros. setoid_rewrite H. trivial. Qed.
+Proof. intros Heq. setoid_rewrite Heq. trivial. Qed.
 
 Lemma project_op (x y: iResUR Σ) γ :
     project (x ⋅ y) γ ≡ project x γ ⋅ project y γ.
 Proof.
   unfold project.
   rewrite lookup_op.
-  destruct (x (inG_id i) !! γ) eqn:p1; destruct (y (inG_id i) !! γ) eqn:p2.
+  destruct (x (inG_id i) !! γ) as [o|] eqn:p1; destruct (y (inG_id i) !! γ) as [o0|] eqn:p2.
   - rewrite p1. rewrite p2.
       replace (Some o ⋅ Some o0) with (Some (o ⋅ o0)) by trivial.
       apply some_op_equiv.
@@ -90,7 +90,7 @@ Lemma discrete_equiv_opt (a b : option A) (n: nat)
   : a ≡{n}≡ b -> a ≡ b.
 Proof using A Disc.
   intro H.
-  destruct a, b.
+  destruct a as [c|], b as [c0|].
   - setoid_replace c with c0; trivial. apply (discrete_equiv _ _ n).
     inversion H. trivial.
   - inversion H.
@@ -107,8 +107,8 @@ Proof.
       { trivial. }
       trivial.
   }
-  destruct (x (inG_id i) !! γ);
-  destruct (y (inG_id i) !! γ).
+  destruct (x (inG_id i) !! γ) as [o|];
+  destruct (y (inG_id i) !! γ) as [o0|].
   - assert (o ≡{n}≡ o0) as Q.
     + unfold "≡" in M. unfold ofe_equiv, optionO, option_equiv in M.
           inversion M. trivial.
@@ -150,7 +150,7 @@ Lemma iRes_incl_from_proj γ x w n :
 Proof.
   intro p.
   unfold project in p.
-  destruct (w (inG_id i) !! γ) eqn:e.
+  destruct (w (inG_id i) !! γ) as [o|] eqn:e.
   - assert ((cmra_transport (eq_sym inG_prf) (own.inG_fold o)) ≡ x) as X.
     { unfold "≡", ofe_equiv, optionO, option_equiv in p. inversion p. trivial. }
     unfold includedN.
@@ -340,11 +340,11 @@ Lemma Some_incl_Some_Some_to_iRes_singleton_incl (a b c : A) n γ
             (sincl: Some a ≼{n} Some b ⋅ Some c) :
             (own.iRes_singleton γ a ≼{n} own.iRes_singleton γ b ⋅ own.iRes_singleton γ c).
 Proof.
-  rewrite <- iRes_singleton_op. destruct sincl as [z sincl]. destruct z.
-  + rewrite some_dot_some in sincl. rewrite some_dot_some in sincl. inversion sincl.
+  rewrite <- iRes_singleton_op. destruct sincl as [z sincl]. destruct z as [c0|].
+  + rewrite some_dot_some in sincl. rewrite some_dot_some in sincl. inversion sincl as [x y Hequ|].
     exists (own.iRes_singleton γ c0). rewrite <- iRes_singleton_op.
-    unfold own.iRes_singleton. f_equiv. apply: singletonM_proper. setoid_rewrite H1. trivial.
-  + rewrite some_dot_some in sincl. rewrite dot_none in sincl. inversion sincl.
+    unfold own.iRes_singleton. f_equiv. apply: singletonM_proper. setoid_rewrite Hequ. trivial.
+  + rewrite some_dot_some in sincl. rewrite dot_none in sincl. inversion sincl as [x y H1|].
     exists ε. rewrite ucmra_unit_right_id.
     unfold own.iRes_singleton. f_equiv. apply: singletonM_proper. setoid_rewrite H1. trivial.
 Qed.
@@ -353,11 +353,11 @@ Lemma Some_incl_Some_None_to_iRes_singleton_incl (a b : A) n γ
             (sincl: Some a ≼{n} Some b ⋅ None) :
             (own.iRes_singleton γ a ≼{n} own.iRes_singleton γ b).
 Proof.
-  destruct sincl as [z sincl]. rewrite dot_none in sincl. destruct z.
-  + rewrite some_dot_some in sincl. inversion sincl. exists (own.iRes_singleton γ c).
+  destruct sincl as [z sincl]. rewrite dot_none in sincl. destruct z as [c|].
+  + rewrite some_dot_some in sincl. inversion sincl as [x y H1|]. exists (own.iRes_singleton γ c).
     rewrite <- iRes_singleton_op. unfold own.iRes_singleton. f_equiv. apply: singletonM_proper.
     setoid_rewrite H1. trivial.
-  + rewrite dot_none in sincl. inversion sincl. exists ε. rewrite ucmra_unit_right_id.
+  + rewrite dot_none in sincl. inversion sincl as [x y H1|]. exists ε. rewrite ucmra_unit_right_id.
     unfold own.iRes_singleton. f_equiv. apply: singletonM_proper. setoid_rewrite H1. trivial.
 Qed.
 
@@ -392,13 +392,13 @@ Proof using A Disc i Σ.
   replace (Some y ⋅ project z2 γ) with (Some (y ⋅? project z2 γ)) in Y.
   2: { unfold "⋅?". destruct (project z2 γ); trivial. }
   
-  destruct (project p1 γ) eqn:p1eqn. 2: { inversion Y. }
+  destruct (project p1 γ) as [c|] eqn:p1eqn. 2: { inversion Y. }
   
-  inversion Y.
+  inversion Y as [x0 y0 R1 R2 R3|].
   
   replace (Some c ⋅ project p2 γ) with (Some (c ⋅? project p2 γ)) in X.
   2: { unfold "⋅?". destruct (project p2 γ); trivial. }
-  inversion X.
+  inversion X as [x1 y1 Q1 Q2 Q3|].
   
   assert (✓ (c ⋅? project p2 γ)) as val2. {
     have vp := valid_project _ γ _ val.
@@ -409,15 +409,15 @@ Proof using A Disc i Σ.
     - destruct (project p2 γ); trivial.
   }
   
-  symmetry in H4. have eq1 := discrete_equiv _ _ _ H4.
-  symmetry in H1. have eq2 := discrete_equiv _ _ _ H1.
+  symmetry in Q1. have eq1 := discrete_equiv _ _ _ Q1.
+  symmetry in R1. have eq2 := discrete_equiv _ _ _ R1.
   have cond0 := cond n c (project p2 γ) (project z1 γ) (project z2 γ) val2 eq1 eq2.
   destruct cond0 as [m [req_eq res_incl]].
   destruct m as [m|].
   2: {
     exists z2. split.
       + symmetry. apply incl2.
-      + unfold includedN in res_incl. destruct res_incl as [z res_incl]. destruct z.
+      + unfold includedN in res_incl. destruct res_incl as [z res_incl]. destruct z as [c0|].
         * rewrite none_dot in res_incl. rewrite some_dot_some in res_incl.
           have ri' := discrete_equiv_opt _ _ _ res_incl.
           have t := iRes_incl_from_proj γ (x ⋅ c0) p2 n ri'.
@@ -443,11 +443,11 @@ Proof using A Disc i Σ.
         unfold "⋅", cmra_op, optionR, option_op_instance, union_with, option_union_with.
         unfold project in p1eqn.
         destruct (p1 (inG_id i) !! γ) eqn:p1eqn'; try discriminate.
-        inversion p1eqn.
+        inversion p1eqn as [J].
         rewrite p1eqn'. f_equiv.
         rewrite <- (cmra_morphism_op _).
         rewrite <- cmra_transport_op.
-        simpl in req_eq. setoid_rewrite req_eq. setoid_rewrite <- H6.
+        simpl in req_eq. setoid_rewrite req_eq. setoid_rewrite <- J.
         rewrite cmra_transport_trans eq_trans_sym_inv_l /=.
         setoid_rewrite own.inG_unfold_fold. 
         trivial.
@@ -461,7 +461,7 @@ Proof using A Disc i Σ.
       setoid_rewrite discrete_fun_lookup_insert_ne; trivial.
       apply ucmra_unit_left_id.
   - have ineq1 := discrete_fun_insert_incl_iRes_singleton n m p1 γ.
-    destruct (project p2 γ) eqn:p2eqn.
+    destruct (project p2 γ) as [c0|] eqn:p2eqn.
     + assert (project p2 γ ≡ Some c0) as p2eqn'. { rewrite p2eqn. trivial. }
       have ineq2 := iRes_incl_from_proj γ c0 p2 n p2eqn'.
       have ineq3 := Some_incl_Some_Some_to_iRes_singleton_incl _ _ _ _ γ res_incl.
@@ -483,7 +483,7 @@ Context `{Disc : CmraDiscrete A}.
 Lemma incl_opq (x: A) (a: option A)
   : x ≼ x ⋅? a.
 Proof.
-  destruct a.
+  destruct a as [u|].
   - unfold "⋅?". unfold "≼". exists u. trivial.
   - unfold "⋅?". unfold "≼". exists ε. symmetry. apply ucmra_unit_right_id.
 Qed.
diff --git a/src/guarding/storage_protocol/base_storage_opt.v b/src/guarding/storage_protocol/base_storage_opt.v
index 506b67c..239c00f 100644
--- a/src/guarding/storage_protocol/base_storage_opt.v
+++ b/src/guarding/storage_protocol/base_storage_opt.v
@@ -1,5 +1,6 @@
 Require Import guarding.storage_protocol.inved.
 Require Import guarding.storage_protocol.protocol.
+From iris.proofmode Require Import base ltac_tactics tactics coq_tactics reduction.
 
 Inductive BaseOpt (S: Type) :=
   | Empty : BaseOpt S
diff --git a/src/guarding/storage_protocol/inved.v b/src/guarding/storage_protocol/inved.v
index 042dfe5..948863d 100644
--- a/src/guarding/storage_protocol/inved.v
+++ b/src/guarding/storage_protocol/inved.v
@@ -1,16 +1,7 @@
-From iris.algebra Require Export cmra updates.
-From iris.algebra Require Import proofmode_classes.
-From iris.algebra Require Import auth.
 From iris.prelude Require Import options.
-
+From iris.algebra Require Export cmra updates proofmode_classes.
 From iris.base_logic.lib Require Export own iprop.
-From iris.proofmode Require Import base.
-From iris.proofmode Require Import ltac_tactics.
-From iris.proofmode Require Import tactics.
-From iris.proofmode Require Import coq_tactics.
-
-From iris.proofmode Require Import coq_tactics reduction.
-From iris.proofmode Require Export tactics.
+From iris.proofmode Require Import base ltac_tactics tactics coq_tactics reduction.
 
 (*
 Context {Σ: gFunctors}.
@@ -81,7 +72,7 @@ Proof.
   unfold "≼".
   unfold "≼" in mle.
   destruct mle as [z mle].
-  destruct z.
+  destruct z as [|p].
   - right. unfold "≡", inved_protocol_equiv, "⋅", inved_protocol_op in mle. trivial.
   - left. exists p.
     unfold "≡", inved_protocol_equiv, "⋅", inved_protocol_op in mle. trivial.
@@ -105,7 +96,7 @@ Global Instance inved_protocol_equivalence
     : Equivalence (≡@{InvedProtocol P}).
 Proof.
   split.
-  - unfold Reflexive. intros. unfold "≡", inved_protocol_equiv. destruct x; trivial.
+  - unfold Reflexive. intros x. unfold "≡", inved_protocol_equiv. destruct x; trivial.
   - unfold Symmetric. intros x y. unfold "≡", inved_protocol_equiv. destruct x, y; trivial.
   - unfold Transitive. intros x y z. 
       unfold "≡", inved_protocol_equiv. destruct x, y, z; trivial.
@@ -133,27 +124,29 @@ Definition inved_protocol_ra_mixin {P}
     {equ: @Equivalence P (≡)}
     (protocol_mixin: ProtocolMixin P) : RAMixin (InvedProtocol P).
 Proof.
-  destruct protocol_mixin.
-  destruct protocol_ra_mixin0.
+  destruct protocol_mixin as [protocol_ra_mixin0
+    protocol_unit_left_id0 inv_implies_valid0 inv_proper0].
+  have protocol_ra_mixin1 := protocol_ra_mixin0.
+  destruct protocol_ra_mixin0 as [ra_op_proper ra_core_proper ra_validN_proper ra_assoc ra_comm ra_pcore_l ra_pcore_idemp ra_pcore_mono ra_valid_op_l].
   split.
- - intro.
+ - intro inved_prot.
     + unfold Proper, equiv, "==>".
       unfold inved_protocol_equiv.
-      intros a b. destruct a; destruct b; unfold "⋅", inved_protocol_op; intro e; destruct x; trivial; try contradiction.
+      intros a b. destruct a; destruct b; unfold "⋅", inved_protocol_op; intro e; destruct inved_prot; trivial; try contradiction.
       eapply ra_op_proper; trivial.
  - intros x y cx e p.
-    destruct x, y.
+    destruct x as [|p0], y as [|p1].
     + exists Nah. split; trivial.
         destruct cx; trivial. unfold pcore, inved_protocol_pcore in p. inversion p.
     + inversion e.
     + inversion e.
     + unfold "≡", inved_protocol_equiv in e.
-        destruct cx.
+        destruct cx as [|p2].
         * unfold pcore, inved_protocol_pcore in p.
           unfold pcore, inved_protocol_pcore.
-          destruct (pcore p0) eqn:l0.
+          destruct (pcore p0) as [p2|] eqn:l0.
           { inversion p. }
-          destruct (pcore p1) eqn:l1.
+          destruct (pcore p1) as [p2|] eqn:l1.
           {
             assert (p1 ≡ p0) as esym. { symmetry. trivial. }
             have t := ra_core_proper p1 p0 p2 esym l1. 
@@ -164,13 +157,13 @@ Proof.
         * 
         have t := ra_core_proper p0 p1 p2 e.
         unfold pcore, inved_protocol_pcore in p.
-        destruct (pcore p0) eqn:q.
+        destruct (pcore p0) as [p3|] eqn:q.
 
         ++ assert (Some p3 = Some p2) as pe. { f_equal. inversion p. trivial. }
           have t0 := t pe. destruct t0 as [cy [t0 t1]]. exists (Inved cy). split.
           ** unfold pcore. unfold inved_protocol_pcore. rewrite t0. trivial.
           ** unfold "≡", inved_protocol_equiv. trivial.
-        ++ destruct (pcore p1) eqn:l1.
+        ++ destruct (pcore p1) as [p3|] eqn:l1.
           {
             assert (p1 ≡ p0) as esym. { symmetry. trivial. }
             have t2 := ra_core_proper p1 p0 p3 esym l1. 
@@ -182,7 +175,7 @@ Proof.
           inversion p. trivial.
     
  - unfold Proper, equiv, impl, "==>". intros x y ipe. unfold "✓", inved_protocol_valid.
-    destruct x; destruct y.
+    destruct x as [|p]; destruct y as [|p0].
     + trivial.
     + inversion ipe.
     + inversion ipe.
@@ -193,25 +186,25 @@ Proof.
       assert (p0 ⋅ b ≡ b ⋅ p0) as Y. { eapply ra_comm. }
       setoid_rewrite X. setoid_rewrite Y.
       eapply ra_op_proper. trivial.
- - unfold Assoc. intros. destruct x, y, z; unfold "⋅"; unfold inved_protocol_op;
+ - unfold Assoc. intros x y z. destruct x, y, z; unfold "⋅"; unfold inved_protocol_op;
     unfold "≡"; unfold inved_protocol_equiv; trivial. (*apply ra_assoc.*)
- - unfold Comm. intros. destruct x, y; unfold "⋅"; unfold inved_protocol_op;
+ - unfold Comm. intros x y. destruct x, y; unfold "⋅"; unfold inved_protocol_op;
     unfold "≡"; unfold inved_protocol_equiv; trivial. (*apply ra_comm.*)
- - intros x cx pc. destruct x, cx.
+ - intros x cx pc. destruct x as [|p], cx as [|p0].
     + trivial.
     + inversion pc.
     + unfold "⋅", inved_protocol_op. unfold "≡", inved_protocol_equiv. trivial.
     + unfold "⋅". unfold inved_protocol_op. unfold "≡". unfold inved_protocol_equiv.
-      unfold pcore, inved_protocol_pcore in pc. destruct (pcore p) eqn:pp.
+      unfold pcore, inved_protocol_pcore in pc. destruct (pcore p) as [p1|] eqn:pp.
       * have t := ra_pcore_l p p1 pp. inversion pc. subst p0. trivial.
       * inversion pc. subst p0. apply protocol_unit_left_id0.
- - intros x cx pc. destruct x, cx.
+ - intros x cx pc. destruct x as [|p], cx as [|p0].
     + unfold pcore. unfold inved_protocol_pcore.
         unfold "≡". unfold option_equiv. apply Some_Forall2. trivial.
     + inversion pc.
     + unfold pcore. unfold inved_protocol_pcore.
         unfold "≡". unfold option_equiv. apply Some_Forall2. trivial.
-    + unfold pcore, inved_protocol_pcore in pc. destruct (pcore p) eqn:pp; try discriminate.
+    + unfold pcore, inved_protocol_pcore in pc. destruct (pcore p) as [p1|] eqn:pp; try discriminate.
       { have t := ra_pcore_idemp p p1 pp.
           inversion pc. subst p0.
           unfold pcore, inved_protocol_pcore. destruct (pcore p1) eqn:pp1.
@@ -221,16 +214,16 @@ Proof.
       }
       {
         inversion pc. subst p0. unfold pcore. unfold inved_protocol_pcore.
-        destruct (pcore ε) eqn:pe; trivial.
-        have ll := ra_pcore_l ε p0 pe.
+        destruct (pcore ε) as [p3|] eqn:pe; trivial.
+        have ll := ra_pcore_l ε p3 pe.
         generalize ll. rewrite ra_comm. rewrite protocol_unit_left_id0. intro mm.
         unfold "≡", option_equiv. apply Some_Forall2. unfold "≡", inved_protocol_equiv.
         trivial.
       }
- - intros x y cx mle pc. destruct x, y.
+ - intros x y cx mle pc. destruct x as [|p], y as [|p0].
     + exists Nah. split; trivial. unfold "≼". exists Nah. inversion pc. subst cx. trivial.
-    + unfold pcore, inved_protocol_pcore. destruct (pcore p).
-        * exists (Inved p0). split; trivial. unfold "≼". exists (Inved p0).
+    + unfold pcore, inved_protocol_pcore. destruct (pcore p0) as [p2|].
+        * exists (Inved p2). split; trivial. unfold "≼". exists (Inved p2).
               inversion pc. subst cx. unfold "⋅", inved_protocol_op.
               unfold "≡". unfold inved_protocol_equiv. trivial.
         * exists (Inved ε). split; trivial.
@@ -241,15 +234,15 @@ Proof.
         unfold inved_protocol_equiv in mle. destruct z; unfold "⋅", inved_protocol_op in mle;
             contradiction.
     + have mle2 := inved_incl_to_incl _ _ mle. destruct mle2 as [mle2|yy].
-        * destruct cx.
-          ++ unfold pcore, inved_protocol_pcore. destruct (pcore p0).
+        * destruct cx as [|p1].
+          ++ unfold pcore, inved_protocol_pcore. destruct (pcore p0) as [p1|].
             ** exists (Inved p1). split; trivial. unfold "≼". exists (Inved p1).
                   inversion pc. unfold "⋅", inved_protocol_op.
                   unfold "≡". unfold inved_protocol_equiv. trivial.
             ** exists (Inved ε). split; trivial. unfold "≼". exists (Inved ε).
                   inversion pc. trivial.
           ++ unfold pcore, inved_protocol_pcore in pc.
-              destruct (pcore p) eqn:pp; try discriminate.
+              destruct (pcore p) as [p2|] eqn:pp; try discriminate.
               { inversion pc. subst p2.
                 have t := ra_pcore_mono p p0 p1 mle2 pp.
                 destruct t as [cy [t1 t2]].
@@ -259,21 +252,21 @@ Proof.
                 ** apply incl_to_inved_incl. trivial.
               }
               { inversion pc. subst p1. unfold pcore, inved_protocol_pcore.
-                destruct (pcore p0).
+                destruct (pcore p0) as [p1|].
                 ** exists (Inved p1). split; trivial. apply incl_to_inved_incl.
                     unfold "≼". exists p1. rewrite protocol_unit_left_id0. trivial.
                 ** exists (Inved ε). split; trivial. apply incl_to_inved_incl.
                     unfold "≼". exists ε. rewrite protocol_unit_left_id0. trivial.
               }
-        * destruct cx.
-          ++ unfold pcore, inved_protocol_pcore. destruct (pcore p0).
+        * destruct cx as [|p1].
+          ++ unfold pcore, inved_protocol_pcore. destruct (pcore p0) as [p1|].
             ** exists (Inved p1). split; trivial. unfold "≼". exists (Inved p1).
                   inversion pc. unfold "⋅", inved_protocol_op.
                   unfold "≡". unfold inved_protocol_equiv. trivial.
             ** exists (Inved ε). split; trivial. unfold "≼". exists (Inved ε).
                   inversion pc. trivial.
           ++ symmetry in yy. unfold pcore, inved_protocol_pcore in pc.
-              destruct (pcore p) eqn:pp; try discriminate.
+              destruct (pcore p) as [p2|] eqn:pp; try discriminate.
              { have j := ra_core_proper p p0 p2 yy pp. destruct j as [cy [j1 j2]].
                 exists (Inved cy).
                 split. { unfold pcore. unfold inved_protocol_pcore. rewrite j1. trivial. }
@@ -281,7 +274,7 @@ Proof.
                 unfold "≼". exists Nah. unfold "⋅". unfold inved_protocol_op.
                 unfold "≡", inved_protocol_equiv. symmetry. trivial.
              }
-             { inversion pc. subst p1. destruct (pcore p0) eqn:pp0.
+             { inversion pc. subst p1. destruct (pcore p0) as [p1|] eqn:pp0.
                 ** assert (p0 ≡ p) as yy_sym by (symmetry; trivial).
                     have j := ra_core_proper p0 p p1 yy_sym pp0. destruct j as [cy [w v]].
                     rewrite w in pp. discriminate.
@@ -290,7 +283,7 @@ Proof.
                     apply incl_to_inved_incl. unfold "≼". exists ε.
                       rewrite protocol_unit_left_id0. trivial.
              }
- - intros x y.  unfold "✓". unfold inved_protocol_valid. destruct x, y.
+ - intros x y.  unfold "✓". unfold inved_protocol_valid. destruct x as [|p], y as [|p0].
     + unfold "⋅", inved_protocol_op. trivial.
     + unfold "⋅", inved_protocol_op. trivial.
     + unfold "⋅", inved_protocol_op. trivial.
diff --git a/src/lang/lang.v b/src/lang/lang.v
index c4d5562..f69bb17 100644
--- a/src/lang/lang.v
+++ b/src/lang/lang.v
@@ -169,7 +169,7 @@ Proof.
   refine (inj_countable'
             (λ l, match l with | LitInt n => inl n | LitUnit => inr () end)
             (λ v, match v with | inl n => _ | inr _ => _ end) _).
-  destruct x; eauto.
+  intro x; destruct x; eauto.
 Qed.
 
 Global Instance bin_op_countable : Countable bin_op.
@@ -178,7 +178,7 @@ Proof.
             (λ op, match op with | PlusOp => 0 | EqOp => 1 | PairOp => 2 | ModuloOp => 3 end)
             (λ n, match n with | 0 => _ | 1 => _ | 2 => _ | 3 => _
                           | _ => ltac:(constructor) end) _).
-  destruct x; eauto.
+  intro x; destruct x; eauto.
 Qed.
 
 Global Instance un_op_countable : Countable un_op.
@@ -186,7 +186,7 @@ Proof.
   refine (inj_countable'
             (λ op, match op with | FstOp => 0 | SndOp => 1  end)
             (λ n, match n with | 0 => _ | 1 => _ | _ => ltac:(constructor) end) _).
-  destruct x; eauto.
+  intro x; destruct x; eauto.
 Qed.
 
 Global Instance heap_op_countable : Countable heap_op.
@@ -195,7 +195,7 @@ Proof.
             (λ op, match op with | AllocOp => 0 | LoadOp => 1 | StoreOp => 2 | FaaOp => 3 | CasOp => 4 | FreeOp => 5 end)
             (λ n, match n with | 0 => _ | 1 => _ | 2 => _ | 3 => _ | 4 => _ | 5 => _
                           | _ => ltac:(constructor) end) _).
-  destruct x; eauto.
+  intro x; destruct x; eauto.
 Qed.
 
 Global Instance expr_countable : Countable expr.