diff --git a/_CoqProject b/_CoqProject
index becfb77f9b2e0858f1f74beb3656838bc04596ef..6d93fb80ae0db49b02edcca5d5aa4dd27cda878d 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -10,4 +10,4 @@ theories/encodings/stype.v
 theories/encodings/stype_enc.v
 theories/examples/examples.v
 theories/examples/proofs.v
-theories/examples/proofs_enc.v
\ No newline at end of file
+theories/examples/proofs_enc.v
diff --git a/theories/encodings/stype.v b/theories/encodings/stype.v
index 0c523a006db6eda3f10f1544e1c2a94df2ab930b..37fb923330bb35dbbda3486679facbed254f0fd6 100644
--- a/theories/encodings/stype.v
+++ b/theories/encodings/stype.v
@@ -79,7 +79,7 @@ Section stype_interp.
                | _ => False
                end
     end%I.
-  Arguments st_eval : simpl nomatch.
+  Global Arguments st_eval : simpl nomatch.
 
   Lemma st_later_eq a P2 (st : stype val (iProp Σ)) st2 :
     (▷ (st ≡ TSR a P2 st2) -∗
@@ -148,7 +148,8 @@ Section stype_interp.
       (c : val) (s : side) : iProp Σ :=
     (st_own γ s st ∗ is_st γ st c)%I.
 
-  Global Instance interp_st_proper γ : Proper ((≡) ==> (=) ==> (=) ==> (≡)) (interp_st γ).
+  Global Instance interp_st_proper γ :
+    Proper ((≡) ==> (=) ==> (=) ==> (≡)) (interp_st γ).
   Proof.
     intros st1 st2 Heq v1 v2 <- s1 s2 <-.
     iSplit;
@@ -163,10 +164,15 @@ Section stype_interp.
     f_equiv;
     apply stype_map_equiv=> //.
   Qed.
+End stype_interp.
 
-  Notation "⟦ c @ s : sτ ⟧{ γ }" := (interp_st γ sτ c s)
+  Notation "⟦ c @ s : sτ ⟧{ N , γ }" := (interp_st N γ sτ c s)
     (at level 10, s at next level, sτ at next level, γ at next level,
-     format "⟦  c  @  s  :  sτ  ⟧{ γ }").
+     format "⟦  c  @  s  :  sτ  ⟧{ N , γ }").
+
+Section stype_specs.
+  Context `{!heapG Σ} (N : namespace).
+  Context `{!logrelG val Σ}.
 
   Lemma new_chan_vs st E c cγ :
     is_chan N cγ c ∗
@@ -175,7 +181,7 @@ Section stype_interp.
     ={E}=∗
       ∃ lγ rγ,
         let γ := SessionType_name cγ lγ rγ in
-        ⟦ c @ Left : st ⟧{γ} ∗ ⟦ c @ Right : dual_stype st ⟧{γ}.
+        ⟦ c @ Left : st ⟧{N,γ} ∗ ⟦ c @ Right : dual_stype st ⟧{N,γ}.
   Proof.
     iIntros "[#Hcctx [Hcol Hcor]]".
     iMod (own_alloc (● (to_stype_auth_excl st) ⋅
@@ -196,8 +202,8 @@ Section stype_interp.
     IsDualStype st1 st2 →
     {{{ True }}}
       new_chan #()
-    {{{ c γ, RET c;  ⟦ c @ Left : st1 ⟧{γ} ∗
-                     ⟦ c @ Right : st2 ⟧{γ} }}}.
+    {{{ c γ, RET c;  ⟦ c @ Left : st1 ⟧{N,γ} ∗
+                     ⟦ c @ Right : st2 ⟧{N,γ} }}}.
   Proof.
     rewrite /IsDualStype.
     iIntros (Hst Φ _) "HΦ".
@@ -210,16 +216,16 @@ Section stype_interp.
     iDestruct "H" as (lγ rγ) "[Hl Hr]".
     iApply "HΦ".
     rewrite Hst.
-    by iFrame.        
+    by iFrame.
   Qed.
 
   Lemma send_vs c γ s (P : val → iProp Σ) st E :
     ↑N ⊆ E →
-    ⟦ c @ s : TSend P st ⟧{γ} ={E,E∖↑N}=∗
+    ⟦ c @ s : TSend P st ⟧{N,γ} ={E,E∖↑N}=∗
       ∃ vs, chan_own (st_c_name γ) s vs ∗
       ▷ (∀ v, P v -∗
               chan_own (st_c_name γ) s (vs ++ [v])
-              ={E∖ ↑N,E}=∗ ⟦ c @ s : st v ⟧{γ}).
+              ={E∖ ↑N,E}=∗ ⟦ c @ s : st v ⟧{N,γ}).
   Proof.
     iIntros (Hin) "[Hstf #[Hcctx Hinv]]".
     iMod (inv_open with "Hinv") as "Hinv'"=> //.
@@ -271,9 +277,9 @@ Section stype_interp.
   Qed.
 
   Lemma send_st_spec st γ c s (P : val → iProp Σ) v :
-    {{{ P v ∗ ⟦ c @ s : TSend P st ⟧{γ} }}}
+    {{{ P v ∗ ⟦ c @ s : TSend P st ⟧{N,γ} }}}
       send c #s v
-    {{{ RET #(); ⟦ c @ s : st v ⟧{γ} }}}.
+    {{{ RET #(); ⟦ c @ s : st v ⟧{N,γ} }}}.
   Proof.
     iIntros (Φ) "[HP Hsend] HΦ".
     iApply (send_spec with "[#]").
@@ -286,14 +292,14 @@ Section stype_interp.
 
   Lemma try_recv_vs c γ s (P : val → iProp Σ) st E :
     ↑N ⊆ E →
-    ⟦ c @ s : TReceive P st ⟧{γ}
+    ⟦ c @ s : TReceive P st ⟧{N,γ}
     ={E,E∖↑N}=∗
       ∃ vs, chan_own (st_c_name γ) (dual_side s) vs ∗
       (▷ ((⌜vs = []⌝ -∗ chan_own (st_c_name γ) (dual_side s) vs ={E∖↑N,E}=∗
-           ⟦ c @ s : TReceive P st ⟧{γ}) ∧
+           ⟦ c @ s : TReceive P st ⟧{N,γ}) ∧
           (∀ v vs', ⌜vs = v :: vs'⌝ -∗
                chan_own (st_c_name γ) (dual_side s) vs' -∗ |={E∖↑N,E}=>
-               ⟦ c @ s : (st v) ⟧{γ} ∗ ▷  P v))).
+               ⟦ c @ s : (st v) ⟧{N,γ} ∗ ▷  P v))).
   Proof.
     iIntros (Hin) "[Hstf #[Hcctx Hinv]]".
     iMod (inv_open with "Hinv") as "Hinv'"=> //.
@@ -358,10 +364,10 @@ Section stype_interp.
   Qed.
 
   Lemma try_recv_st_spec st γ c s (P : val → iProp Σ) :
-    {{{ ⟦ c @ s : TReceive P st ⟧{γ} }}}
+    {{{ ⟦ c @ s : TReceive P st ⟧{N,γ} }}}
       try_recv c #s
-    {{{ v, RET v; (⌜v = NONEV⌝ ∧ ⟦ c @ s : TReceive P st ⟧{γ}) ∨
-                  (∃ w, ⌜v = SOMEV w⌝ ∧ ⟦ c @ s : st w ⟧{γ} ∗ ▷ P w)}}}.
+    {{{ v, RET v; (⌜v = NONEV⌝ ∧ ⟦ c @ s : TReceive P st ⟧{N,γ}) ∨
+                  (∃ w, ⌜v = SOMEV w⌝ ∧ ⟦ c @ s : st w ⟧{N,γ} ∗ ▷ P w)}}}.
   Proof.
     iIntros (Φ) "Hrecv HΦ".
     iApply (try_recv_spec with "[#]").
@@ -387,9 +393,9 @@ Section stype_interp.
   Qed.
 
   Lemma recv_st_spec st γ c s (P : val → iProp Σ) :
-    {{{ ⟦ c @ s : TReceive P st ⟧{γ} }}}
+    {{{ ⟦ c @ s : TReceive P st ⟧{N,γ} }}}
       recv c #s
-    {{{ v, RET v; ⟦ c @ s : st v ⟧{γ} ∗ P v}}}.
+    {{{ v, RET v; ⟦ c @ s : st v ⟧{N,γ} ∗ P v}}}.
   Proof.
     iIntros (Φ) "Hrecv HΦ".
     iLöb as "IH". wp_rec.
@@ -407,4 +413,4 @@ Section stype_interp.
       iFrame.
   Qed.
 
-End stype_interp.
\ No newline at end of file
+End stype_specs.
\ No newline at end of file
diff --git a/theories/encodings/stype_enc.v b/theories/encodings/stype_enc.v
index 5c16849ebc294a8e8862c6d001d24311cc6b3c2d..ccfc32c6f31455a68f92d28f293bfaef93111c4e 100644
--- a/theories/encodings/stype_enc.v
+++ b/theories/encodings/stype_enc.v
@@ -70,18 +70,15 @@ Proof.
     apply decenc. eauto.
 Qed.
 
-Definition TSR' `{PROP: bi} {V} `{ED : EncDec V}
+Section DualStypeEnc.
+  Context `{EncDec V} `{PROP: bi} .
+
+  Definition TSR'
     (a : action) (P : V → PROP) (st : V → stype val PROP) : stype val PROP :=
   TSR a
     (λ v, if decode v is Some x then P x else False)%I
     (λ v, if decode v is Some x then st x else TEnd (* dummy *)).
-Instance: Params (@TSR') 4.
-
-Notation TSend P st := (TSR' Send P st).
-Notation TReceive P st := (TSR' Receive P st).
-
-Section DualStypeEnc.
-  Context `{PROP: bi} `{EncDec V}.
+  Global Instance: Params (@TSR') 3.
 
   Global Instance is_dual_tsr' a1 a2 P (st1 st2 : V → stype val PROP) :
     IsDualAction a1 a2 →
@@ -92,44 +89,20 @@ Section DualStypeEnc.
     constructor=> x. done. by destruct (decode x).
   Qed.
 
-  Global Instance is_dual_send P (st1 st2 : V → stype val PROP) :
-    (∀ x, IsDualStype (st1 x) (st2 x)) →
-    IsDualStype (TSend P st1) (TReceive P st2).
-  Proof. intros Heq. by apply is_dual_tsr'. Qed.
-  
-  Global Instance is_dual_receive P (st1 st2 : V → stype val PROP) :
-    (∀ x, IsDualStype (st1 x) (st2 x)) →
-    IsDualStype (TReceive P st1) (TSend P st2).
-  Proof. intros Heq. by apply is_dual_tsr'. Qed.
-
 End DualStypeEnc.
 
-Section Encodings.
+Notation TSend := (TSR' Send).
+Notation TReceive := (TSR' Receive).
+
+Section stype_enc_specs.
   Context `{!heapG Σ} (N : namespace).
   Context `{!logrelG val Σ}.
 
-  Example ex_st : stype val (iProp Σ) :=
-    (TReceive
-          (λ v', ⌜v' = 5⌝%I)
-          (λ v', TEnd)).
-
-  Example ex_st2 : stype val (iProp Σ) :=
-    TSend
-         (λ b, ⌜b = true⌝%I)
-         (λ b,
-          (TReceive
-              (λ v', ⌜(v' > 5) = b⌝%I)
-              (λ _, TEnd))).
-
-  Notation "⟦ c @ s : sτ ⟧{ γ }" := (interp_st N γ sτ c s)
-    (at level 10, s at next level, sτ at next level, γ at next level,
-     format "⟦  c  @  s  :  sτ  ⟧{ γ }").
-
   Lemma send_st_spec (A : Type) `{EncDec A}
         st γ c s (P : A → iProp Σ) w :
-    {{{ P w ∗ ⟦ c @ s : (TSend P st) ⟧{γ} }}}
+    {{{ P w ∗ ⟦ c @ s : (TSend P st) ⟧{N,γ} }}}
       send c #s (encode w)
-    {{{ RET #(); ⟦ c @ s : st w ⟧{γ} }}}.
+    {{{ RET #(); ⟦ c @ s : st w ⟧{N,γ} }}}.
   Proof.
     iIntros (Φ) "[HP Hsend] HΦ".
     iApply (send_st_spec with "[HP Hsend]").
@@ -143,9 +116,9 @@ Section Encodings.
 
   Lemma recv_st_spec (A : Type) `{EncDec A}
         st γ c s (P : A → iProp Σ) :
-    {{{ ⟦ c @ s : (TReceive P st) ⟧{γ} }}}
+    {{{ ⟦ c @ s : (TReceive P st) ⟧{N,γ} }}}
       recv c #s
-    {{{ v, RET (encode v); ⟦ c @ s : st v ⟧{γ} ∗ P v }}}.
+    {{{ v, RET (encode v); ⟦ c @ s : st v ⟧{N,γ} ∗ P v }}}.
   Proof.
     iIntros (Φ) "Hrecv HΦ".
     iApply (recv_st_spec with "Hrecv").
@@ -164,4 +137,4 @@ Section Encodings.
     - inversion Hw.
   Qed.
 
-End Encodings.
\ No newline at end of file
+End stype_enc_specs.
\ No newline at end of file
diff --git a/theories/examples/examples.v b/theories/examples/examples.v
index 6c500d26209e31d7496b5db70855a4f1549a462a..f5db63f211838b64214438b67c174c7e9ae99b51 100644
--- a/theories/examples/examples.v
+++ b/theories/examples/examples.v
@@ -52,5 +52,5 @@ Section Examples.
      let: "c'" := new_chan #() in
      Fork(recv "c" #Right;; send "c'" #Right #5);;
      recv "c'" #Left;; send "c" #Left #5)%E.
-
+  
 End Examples.
\ No newline at end of file
diff --git a/theories/examples/proofs_enc.v b/theories/examples/proofs_enc.v
index 3644d7a9e1a5ab9ba1de70f7bfdd92098f920c13..8b943debba02f37ba764ad6564d0b8167187fe52 100644
--- a/theories/examples/proofs_enc.v
+++ b/theories/examples/proofs_enc.v
@@ -10,24 +10,20 @@ Section ExampleProofsEnc.
   Context `{!heapG Σ} (N : namespace).
   Context `{!logrelG val Σ}.
 
-  Notation "⟦ c @ s : sτ ⟧{ γ }" := (interp_st N γ sτ c s)
-    (at level 10, s at next level, sτ at next level, γ at next level,
-     format "⟦  c  @  s  :  sτ  ⟧{ γ }").
-  
   Lemma seq_proof :
     {{{ True }}} seq_example {{{ v, RET v; ⌜v = #5⌝ }}}.
   Proof.
     iIntros (Φ H) "HΦ".
     rewrite /seq_example.
     wp_apply (new_chan_st_spec N
-             (TSend (λ v, ⌜v = 5⌝%I) (λ v, TEnd)))=> //.
+             (TSend (λ v, ⌜v = 5⌝%I) (λ v, TEnd)))=> //;
     iIntros (c γ) "[Hstl Hstr]"=> /=.
     wp_apply (send_st_spec N Z with "[$Hstl //]");
     iIntros "Hstl".
     wp_apply (recv_st_spec N Z with "[Hstr]"). iApply "Hstr".
     iIntros (v) "[Hstr HP]".
     iApply "HΦ".
-    iDestruct "HP" as %->.    
+    iDestruct "HP" as %->.
     eauto.
   Qed.
 
@@ -92,7 +88,7 @@ Section ExampleProofsEnc.
       (TSend (λ v, ∃ γ, ⟦ v @ Right :
         (TReceive
           (λ v, ⌜v = 5⌝)
-          (λ _, TEnd)) ⟧{γ})%I
+          (λ _, TEnd)) ⟧{N, γ})%I
       (λ v, TEnd)))=> //;
     iIntros (c γ) "[Hstl Hstr]"=> /=.
     wp_apply (wp_fork with "[Hstl]").
@@ -123,9 +119,9 @@ Section ExampleProofsEnc.
     wp_apply (new_chan_st_spec N
                (TSend (λ v, ⌜v = 5⌝%I) (λ v, TEnd)))=> //;
     iIntros (c γ) "[Hstl Hstr]"=> /=.
-    wp_apply (recv_st_spec _ with "Hstr");
+    wp_apply (recv_st_spec N Z with "Hstr");
     iIntros (v) "[Hstr HP]".
-    wp_apply (send_st_spec N with "[$Hstl //]");
+    wp_apply (send_st_spec N Z with "[$Hstl //]");
     iIntros "Hstl".
     iDestruct "HP" as %->.
     wp_pures.
@@ -161,10 +157,10 @@ Section ExampleProofsEnc.
     wp_apply (wp_fork with "[Hstr Hstr']").
     - iNext. wp_apply (recv_st_spec _ with "Hstr");
       iIntros (v) "[Hstr HP]".
-      wp_apply (send_st_spec _ with "[$Hstr' //]"). eauto.
-    - wp_apply (recv_st_spec _ with "[$Hstl' //]");
+      wp_apply (send_st_spec _ Z with "[$Hstr' //]"). eauto.
+    - wp_apply (recv_st_spec _ Z with "[$Hstl' //]");
       iIntros (v) "[Hstl' HP]".
-      wp_apply (send_st_spec _ with "[$Hstl //]");
+      wp_apply (send_st_spec _ Z with "[$Hstl //]");
       iIntros "Hstl".
       by iApply "HΦ".
   Qed.
diff --git a/theories/typing/stype.v b/theories/typing/stype.v
index 24c27cc7313a45f2cada52ab0ed9d6ab97c7f9a4..d6e5d17f928d6d4f62a38da784ecd30507621d3d 100644
--- a/theories/typing/stype.v
+++ b/theories/typing/stype.v
@@ -14,15 +14,6 @@ Definition dual_action (a : action) : action :=
 Instance dual_action_involutive : Involutive (=) dual_action.
 Proof. by intros []. Qed.
 
-Class IsDualAction (a1 a2 : action) :=
-  is_dual_action : dual_action a1 = a2.
-Instance is_dual_action_default : IsDualAction a (dual_action a) | 100.
-Proof. done. Qed.
-Instance is_dual_action_Send : IsDualAction Send Receive.
-Proof. done. Qed.
-Instance is_dual_action_Receive : IsDualAction Receive Send.
-Proof. done. Qed.
-
 Inductive stype (V A : Type) :=
   | TEnd
   | TSR (a : action) (P : V → A) (st : V → stype V A).
@@ -53,7 +44,7 @@ Section stype_ofe.
        pointwise_relation V (≡) st1 st2 →
        TSR a P1 st1 ≡ TSR a P2 st2.
   Existing Instance stype_equiv.
-    
+
   Inductive stype_dist' (n : nat) : relation (stype V A) :=
     | TEnd_dist : stype_dist' n TEnd TEnd
     | TSR_dist a P1 P2 st1 st2 :
@@ -227,20 +218,29 @@ Proof.
   by intros ? A1 A2 B1 B2 n f g Hfg; apply stypeC_map_ne, cFunctor_contractive.
 Qed.
 
-Class IsDualStype {V} {A : ofeT} (st1 st2 : stype V A) :=
-  is_dual_stype : dual_stype st1 ≡ st2.
+Class IsDualAction (a1 a2 : action) :=
+  is_dual_action : dual_action a1 = a2.
+Instance is_dual_action_default : IsDualAction a (dual_action a) | 100.
+Proof. done. Qed.
+Instance is_dual_action_Send : IsDualAction Send Receive.
+Proof. done. Qed.
+Instance is_dual_action_Receive : IsDualAction Receive Send.
+Proof. done. Qed.
 
 Section DualStype.
-  Context `{PROP: bi} {V : Type}.
+  Context {V : Type} {A : ofeT}.
+
+  Class IsDualStype (st1 st2 : stype V A) :=
+  is_dual_stype : dual_stype st1 ≡ st2.
 
-  Global Instance is_dual_default (st : stype V PROP) :
+  Global Instance is_dual_default (st : stype V A) :
     IsDualStype st (dual_stype st) | 100.
   Proof. by rewrite /IsDualStype. Qed.
 
-  Global Instance is_dual_end : IsDualStype (TEnd : stype V PROP) TEnd.
+  Global Instance is_dual_end : IsDualStype (TEnd : stype V A) TEnd.
   Proof. constructor. Qed.
 
-  Global Instance is_dual_tsr a1 a2 P (st1 st2 : V → stype V PROP) :
+  Global Instance is_dual_tsr a1 a2 P (st1 st2 : V → stype V A) :
     IsDualAction a1 a2 →
     (∀ x, IsDualStype (st1 x) (st2 x)) →
     IsDualStype (TSR a1 P st1) (TSR a2 P st2).
@@ -248,15 +248,5 @@ Section DualStype.
     rewrite /IsDualAction /IsDualStype. intros <- Hst.
     by constructor=> x.
   Qed.
-  
-  Global Instance is_dual_send P (st1 st2 : V → stype V PROP) :
-    (∀ x, IsDualStype (st1 x) (st2 x)) →
-    IsDualStype (TSR Send P st1) (TSR Receive P st2).
-  Proof. intros H. by apply is_dual_tsr. Qed.
-  
-  Global Instance is_dual_receive P (st1 st2 : V → stype V PROP) :
-    (∀ x, IsDualStype (st1 x) (st2 x)) →
-    IsDualStype (TSR Receive P st1) (TSR Send P st2).
-  Proof. intros H. by apply is_dual_tsr. Qed.
 
 End DualStype.
\ No newline at end of file