diff --git a/theories/encodings/auth_excl.v b/theories/encodings/auth_excl.v
index 9aa43fe164a4c0661866af3df7c501e5074e3c20..ddd2611be56d3d8da02cc54fb3a40c66b43203f2 100644
--- a/theories/encodings/auth_excl.v
+++ b/theories/encodings/auth_excl.v
@@ -38,11 +38,11 @@ Section auth_excl.
     ✓ (● to_auth_excl x ⋅ ◯ to_auth_excl y) -∗ (x ≡ y : iProp Σ).
   Proof.
     iIntros "Hvalid".
-    iDestruct (auth_validI with "Hvalid") as "[Hy Hvalid]"; simpl.
-    iDestruct "Hy" as ([z|]) "Hy"; last first.
-    - by rewrite left_id right_id_L bi.option_equivI /= excl_equivI.
+    iDestruct (auth_both_validI with "Hvalid") as "[_ [Hle Hvalid]]"; simpl.
+    iDestruct "Hle" as ([z|]) "Hy"; last first.
+    - by rewrite bi.option_equivI /= excl_equivI.
     - iRewrite "Hy" in "Hvalid".
-      by rewrite left_id uPred.option_validI /= excl_validI /=.
+      by rewrite uPred.option_validI /= excl_validI /=.
   Qed.
 
   Lemma excl_eq γ x y :
@@ -64,4 +64,4 @@ Section auth_excl.
       eapply exclusive_local_update. done. }
     by rewrite own_op.
   Qed.
-End auth_excl.
\ No newline at end of file
+End auth_excl.
diff --git a/theories/encodings/channel.v b/theories/encodings/channel.v
index 5f9e8dd581580e04dca3c8e160df51926f665b05..fa0ed8a70d9937e4154f3fe73410bfd9c489ace7 100644
--- a/theories/encodings/channel.v
+++ b/theories/encodings/channel.v
@@ -121,10 +121,10 @@ Section channel.
     wp_lam.
     wp_apply (lnil_spec with "[//]"); iIntros (ls). wp_alloc l as "Hl".
     wp_apply (lnil_spec with "[//]"); iIntros (rs). wp_alloc r as "Hr".
-    iMod (own_alloc (● (to_auth_excl []) ⋅ ◯ (to_auth_excl [])))
-      as (lsγ) "[Hls Hls']"; first done.
-    iMod (own_alloc (● (to_auth_excl []) ⋅ ◯ (to_auth_excl [])))
-      as (rsγ) "[Hrs Hrs']"; first done.
+    iMod (own_alloc (● (to_auth_excl []) ⋅ ◯ (to_auth_excl []))) as (lsγ) "[Hls Hls']".
+    { by apply auth_both_valid. }
+    iMod (own_alloc (● (to_auth_excl []) ⋅ ◯ (to_auth_excl []))) as (rsγ) "[Hrs Hrs']".
+    { by apply auth_both_valid. }
     iAssert (is_list_ref #l []) with "[Hl]" as "Hl".
     { rewrite /is_list_ref; eauto. }
     iAssert (is_list_ref #r []) with "[Hr]" as "Hr".
diff --git a/theories/encodings/stype.v b/theories/encodings/stype.v
index dd4528e175307cd6ca0a65e9aafd6f2a60d162e9..bef61537337d2f235365d135504b4766050f6104 100644
--- a/theories/encodings/stype.v
+++ b/theories/encodings/stype.v
@@ -185,11 +185,11 @@ Section stype_specs.
   Proof.
     iIntros "[#Hcctx [Hcol Hcor]]".
     iMod (own_alloc (● (to_stype_auth_excl st) ⋅
-                     â—¯ (to_stype_auth_excl st)))
-      as (lγ) "[Hlsta Hlstf]"; first done.
+                     ◯ (to_stype_auth_excl st))) as (lγ) "[Hlsta Hlstf]".
+    { by apply auth_both_valid_2. }
     iMod (own_alloc (● (to_stype_auth_excl (dual_stype st)) ⋅
-                     â—¯ (to_stype_auth_excl (dual_stype st))))
-      as (rγ) "[Hrsta Hrstf]"; first done.
+                     ◯ (to_stype_auth_excl (dual_stype st)))) as (rγ) "[Hrsta Hrstf]".
+    { by apply auth_both_valid_2. }
     pose (SessionType_name cγ lγ rγ) as stγ.
     iMod (inv_alloc N _ (inv_st stγ c) with "[-Hlstf Hrstf Hcctx]") as "#Hinv".
     { iNext. rewrite /inv_st. eauto 10 with iFrame. }