diff --git a/src/Examples/Call.agda b/src/Examples/Call.agda
index 8546c69..70da44b 100644
--- a/src/Examples/Call.agda
+++ b/src/Examples/Call.agda
@@ -4,67 +4,114 @@ open import ActorMonad public
 open import Data.List using (List ; _∷_ ; [] ; _++_)
 open import Data.List.All using (All ; _∷_ ; [])
 open import Data.Bool using (Bool ; if_then_else_ ; false ; true)
-open import Data.Nat using (ℕ ; zero ; suc ; _+_)
+open import Data.Nat using (ℕ ; zero ; suc ; _+_ ; _≟_)
 open import Coinduction
 open import Level using (Lift ; lift) renaming (zero to lzero ; suc to lsuc)
 open import Data.List.Any using (here ; there)
-open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; cong ; sym ; inspect ; [_] ; trans)
-open import Membership using (_∈_ ; _⊆_ ; S ; Z ; _∷_ ; [] ; ⊆-refl ; ⊆-trans ; ⊆-suc ; translate-⊆)
+open import Relation.Binary.PropositionalEquality
+            using (_≡_ ; refl ; cong ; sym ; inspect ; [_] ; trans)
+open import Membership using (
+            _∈_ ; _⊆_ ; S ; Z ; _∷_ ; [] ; ⊆-refl
+            ; ⊆-trans ; ⊆-suc ; translate-⊆)
 open import Data.Unit using (⊤ ; tt)
-open import Examples.SelectiveReceive  using (selective-receive ; SelRec ; waiting-refs ; add-references++ ; ∈-inc ; ⊆++-refl)
+open import Examples.SelectiveReceive using (
+            selective-receive ; SelRec ; waiting-refs
+            ; add-references++ ; ∈-inc ; ⊆++-refl)
+open import Relation.Nullary using (yes ; no)
 
 open import Size
 
 open SelRec
 
-call-select-unwrap : ∀ {MtIn MT} {IS : InboxShape} → MT ∈ IS → MtIn ∈ IS → Bool
-call-select-unwrap Z Z = true
-call-select-unwrap Z (S p) = false
-call-select-unwrap (S x) Z = false
-call-select-unwrap (S x) (S p) = call-select-unwrap x p
+UniqueTag = ℕ
 
-call-select : ∀ {IS IS' MtIn} → IS' <: IS → MtIn ∈ IS' → Message IS → Bool
-call-select sub which (Msg x x₁) = call-select-unwrap x (translate-⊆  sub which)
+call-select-unwrap : ∀ {MtIn MT} {IS : InboxShape} →
+                     UniqueTag →
+                     MT ∈ IS →
+                     All receive-field-content MT →
+                     (ValueType UniqueTag ∷ MtIn) ∈ IS →
+                     Bool
+call-select-unwrap tag Z (tag' ∷ fs) Z with (tag ≟ tag')
+... | yes p = true
+... | no p = false
+call-select-unwrap _ Z _ (S p) = false
+call-select-unwrap _ (S x) _ Z = false
+call-select-unwrap tag (S x) fs (S p) = call-select-unwrap tag x fs p
 
-call : ∀ {Γ MtTo MtIn i} {To IS IS' : InboxShape} → (q : List (Message IS)) → (Γ ⊢ To) →
-       ((ReferenceType IS' ∷ MtTo) ∈ To) → All (send-field-content Γ) MtTo →
-       (ISsubs : IS' <: IS) → (whichIn : MtIn ∈ IS') →
-       ∞ActorM i IS (SelRec IS (call-select ISsubs whichIn)) (Γ ++ (waiting-refs q)) (λ m → (add-references Γ (msg m)) ++ (waiting-refs (waiting m)))
-call {Γ} {IS = IS} q var toFi vals sub whichIn = do
+call-select : ∀ {IS IS' MtIn} →
+              UniqueTag →
+              IS' <: IS →
+              (ValueType UniqueTag ∷ MtIn) ∈ IS' →
+              Message IS →
+              Bool
+call-select tag sub which (Msg x fs) =
+  call-select-unwrap tag x fs (translate-⊆  sub which)
+
+call : ∀ {Γ MtTo MtIn i} {To IS IS' : InboxShape} →
+       (q : List (Message IS)) →
+       (Γ ⊢ To) →
+       ((ValueType UniqueTag ∷ ReferenceType IS' ∷ MtTo) ∈ To) →
+       (tag : UniqueTag) →
+       All (send-field-content Γ) MtTo →
+       (ISsubs : IS' <: IS) →
+       (whichIn : (ValueType UniqueTag ∷ MtIn) ∈ IS') →
+       ∞ActorM i IS
+         (SelRec IS (call-select tag ISsubs whichIn))
+         (Γ ++ (waiting-refs q))
+         (λ m → (add-references Γ (msg m)) ++ (waiting-refs (waiting m)))
+call {Γ} {IS = IS} q var toFi tag vals sub whichIn = do
      self
-     S (translate-⊆ (⊆++-refl Γ (waiting-refs q)) var) ![t: toFi ] (([ Z ]>: sub) ∷ (translate-fields vals))
+     S (translate-⊆ (⊆++-refl Γ (waiting-refs q)) var)
+       ![t: toFi ]
+       ((lift tag) ∷ ([ Z ]>: sub) ∷ (translate-fields vals))
      strengthen (⊆-suc ⊆-refl)
-     selective-receive q (call-select sub whichIn)
+     selective-receive q (call-select tag sub whichIn)
   where
-    translate-fields : ∀ {MT} → All (send-field-content  Γ) MT → All (send-field-content (IS ∷ Γ ++ waiting-refs q)) MT
+    translate-fields : ∀ {MT} → All (send-field-content  Γ) MT →
+                         All (send-field-content (IS ∷ Γ ++ waiting-refs q)) MT
     translate-fields {[]} [] = []
-    translate-fields {ValueType x ∷ MT} (px ∷ ps) = px ∷ translate-fields ps
-    translate-fields {ReferenceType x ∷ MT} (([ p ]>: v) ∷ ps) = ([ (S (∈-inc Γ (waiting-refs q) _ p)) ]>: v) ∷ (translate-fields ps)
+    translate-fields {ValueType x ∷ MT} (px ∷ ps) =
+      px ∷ translate-fields ps
+    translate-fields {ReferenceType x ∷ MT} (([ p ]>: v) ∷ ps) =
+      ([ (S (∈-inc Γ (waiting-refs q) _ p)) ]>: v) ∷ (translate-fields ps)
 
 Calculator : InboxShape
-Calculator = (ReferenceType ((ValueType ℕ ∷ []) ∷ []) ∷ ValueType ℕ ∷ ValueType ℕ ∷ []) ∷ []
+Calculator = (
+  ValueType UniqueTag ∷
+  ReferenceType ((
+    ValueType UniqueTag ∷
+    ValueType ℕ ∷ []) ∷ []
+  ) ∷
+  ValueType ℕ ∷
+  ValueType ℕ ∷ []
+  ) ∷ []
 
 calculatorActor : ∀ {i} → ∞ActorM (↑ i) Calculator (Lift ⊤) [] (λ _ → [])
 calculatorActor = loop
   where
     loop : ∀ {i} → ∞ActorM i Calculator (Lift ⊤) [] (λ _ → [])
     loop .force = receive ∞>>= λ {
-      (Msg Z (_ ∷ n ∷ m ∷ [])) → do
-        Z ![t: Z ] ((lift (n + m)) ∷ [])
+      (Msg Z (tag ∷ _ ∷ n ∷ m ∷ [])) → do
+        Z ![t: Z ] ((lift tag) ∷ (lift (n + m)) ∷ [])
         strengthen []
         loop
       ; (Msg (S ()) _) }
 
 TestBox : InboxShape
-TestBox = ((ValueType ℕ ∷ [])) ∷ [] ∷ []
+TestBox = ((ValueType UniqueTag ∷ ValueType ℕ ∷ [])) ∷ [] ∷ []
 
 calltestActor : ∀ {i} → ∞ActorM i TestBox (Lift ℕ) [] (λ _ → [])
 calltestActor .force = spawn∞ calculatorActor ∞>>
-                       [mid: (λ m → add-references (Calculator ∷ []) (msg m) ++ waiting-refs (waiting m)) ] call [] Z Z ((lift 10) ∷ ((lift 32) ∷ [])) (Z ∷ []) Z >>=
+                       [mid: (λ m → add-references (Calculator ∷ []) (msg m) ++
+                                    waiting-refs (waiting m)) ]
+                         call [] Z Z 0
+                           ((lift 10) ∷ ((lift 32) ∷ []))
+                           (Z ∷ []) Z >>=
                        λ x → strengthen [] >>
                        return-result x
   where
-    return-result : SelRec TestBox (call-select (Z ∷ []) Z) → ∀ {i} → ∞ActorM i TestBox (Lift ℕ) [] (λ _ → [])
-    return-result record { msg = (Msg Z (px ∷ x₁)) } = return px
+    return-result : SelRec TestBox (call-select 0 (Z ∷ []) Z) →
+                    ∀ {i} → ∞ActorM i TestBox (Lift ℕ) [] (λ _ → [])
+    return-result record { msg = (Msg Z (tag ∷ n ∷ [])) } = return n
     return-result record { msg = (Msg (S x) x₁) ; msg-ok = () }
 
diff --git a/src/Selective/Examples/Call.agda b/src/Selective/Examples/Call.agda
index 2286a20..4db6e19 100644
--- a/src/Selective/Examples/Call.agda
+++ b/src/Selective/Examples/Call.agda
@@ -4,64 +4,103 @@ open import Selective.ActorMonad public
 open import Data.List using (List ; _∷_ ; [] ; _++_)
 open import Data.List.All using (All ; _∷_ ; [])
 open import Data.Bool using (Bool ; if_then_else_ ; false ; true)
-open import Data.Nat using (ℕ ; zero ; suc ; _+_)
+open import Data.Nat using (ℕ ; zero ; suc ; _+_ ; _≟_ )
 open import Size
 open import Level using (Lift ; lift) renaming (zero to lzero ; suc to lsuc)
 open import Data.List.Any using (here ; there)
-open import Relation.Binary.PropositionalEquality using (_≡_ ; refl ; cong ; sym ; inspect ; [_] ; trans)
-open import Membership using (_∈_ ; _⊆_ ; S ; Z ; _∷_ ; [] ; ⊆-refl ; ⊆-trans ; ⊆-suc ; translate-⊆)
+open import Relation.Binary.PropositionalEquality
+            using (_≡_ ; refl ; cong ; sym ; inspect ; [_] ; trans)
+open import Membership using (
+              _∈_ ; _⊆_ ; S ; Z ; _∷_ ; []
+              ; ⊆-refl ; ⊆-trans ; ⊆-suc ; translate-⊆
+              )
 open import Data.Unit using (⊤ ; tt)
+open import Relation.Nullary using (yes ; no)
 
 open SelectedMessage
 
-call-select-unwrap : ∀ {MtIn MT} {IS : InboxShape} → MT ∈ IS → MtIn ∈ IS → Bool
-call-select-unwrap Z Z = true
-call-select-unwrap Z (S p) = false
-call-select-unwrap (S x) Z = false
-call-select-unwrap (S x) (S p) = call-select-unwrap x p
+UniqueTag = ℕ
 
-call-select : ∀ {IS IS' MtIn} → IS' <: IS → MtIn ∈ IS' → MessageFilter IS
-call-select {IS} sub which = filter
-  where
-    filter : MessageFilter IS
-    filter (Msg x x₁) = call-select-unwrap x (translate-⊆  sub which)
+call-select-unwrap : ∀ {MtIn MT} {IS : InboxShape} →
+                       UniqueTag →
+                       MT ∈ IS →
+                       All receive-field-content MT →
+                       (ValueType UniqueTag ∷ MtIn) ∈ IS →
+                       Bool
+call-select-unwrap tag Z (tag' ∷ fs) Z with (tag ≟ tag')
+... | yes p = true
+... | no p = false
+call-select-unwrap _ Z _ (S p) = false
+call-select-unwrap _ (S x) _ Z = false
+call-select-unwrap tag (S x) fs (S p) = call-select-unwrap tag x fs p
+
+call-select : ∀ {IS IS' MtIn} →
+                UniqueTag →
+                IS' <: IS →
+                (ValueType UniqueTag ∷ MtIn) ∈ IS' →
+                MessageFilter IS
+call-select {IS} tag sub which (Msg x fs) =
+  call-select-unwrap tag x fs (translate-⊆  sub which)
 
-call : ∀ {Γ MtTo MtIn i} {To IS IS' : InboxShape} → (Γ ⊢ To) →
-       ((ReferenceType IS' ∷ MtTo) ∈ To) → All (send-field-content Γ) MtTo →
-       (ISsubs : IS' <: IS) → (whichIn : MtIn ∈ IS') →
-       ∞ActorM i IS (SelectedMessage (call-select ISsubs whichIn)) Γ (add-selected-references Γ)
-call {Γ} {IS = IS} var toFi vals sub whichIn =
-  self >>
-  ((S var ![t: toFi ] (([ Z ]>: sub) ∷ (translate-fields vals))) >>
-  (strengthen (⊆-suc ⊆-refl) >>
-  selective-receive (call-select sub whichIn)))
+call : ∀ {Γ MtTo MtIn i} {To IS IS' : InboxShape} →
+       (Γ ⊢ To) →
+       ((ValueType UniqueTag ∷ ReferenceType IS' ∷ MtTo) ∈ To) →
+       (tag : UniqueTag) →
+       All (send-field-content Γ) MtTo →
+       (ISsubs : IS' <: IS) →
+       (whichIn : (ValueType UniqueTag ∷ MtIn) ∈ IS') →
+       ∞ActorM i IS
+         (SelectedMessage (call-select tag ISsubs whichIn))
+         Γ (add-selected-references Γ)
+call {Γ} {IS = IS} var toFi tag vals sub whichIn = do
+     self
+     S var ![t: toFi ] ((lift tag) ∷ ([ Z ]>: sub) ∷ (translate-fields vals))
+     strengthen (⊆-suc ⊆-refl)
+     selective-receive (call-select tag sub whichIn)
   where
-    translate-fields : ∀ {MT} → All (send-field-content Γ) MT → All (send-field-content (IS ∷ Γ)) MT
+    translate-fields : ∀ {MT} →
+                       All (send-field-content Γ) MT →
+                       All (send-field-content (IS ∷ Γ)) MT
     translate-fields [] = []
-    translate-fields {ValueType x ∷ MT} (px ∷ vals) = px ∷ (translate-fields vals)
-    translate-fields {ReferenceType x ∷ MT} (([ p ]>: v) ∷ vals) = ([ (S p) ]>: v) ∷ (translate-fields vals)
+    translate-fields {ValueType x ∷ MT} (px ∷ vals) =
+      px ∷ (translate-fields vals)
+    translate-fields {ReferenceType x ∷ MT} (([ p ]>: v) ∷ vals) =
+      ([ (S p) ]>: v) ∷ (translate-fields vals)
 
 Calculator : InboxShape
-Calculator = (ReferenceType ((ValueType ℕ ∷ []) ∷ []) ∷ ValueType ℕ ∷ ValueType ℕ ∷ []) ∷ []
+Calculator = (
+  ValueType UniqueTag ∷
+  ReferenceType ((
+    ValueType UniqueTag ∷
+    ValueType ℕ ∷ []) ∷ []
+  ) ∷
+  ValueType ℕ ∷
+  ValueType ℕ ∷ []
+  ) ∷ []
 
 calculatorActor : ∀ {i} → ∞ActorM (↑ i) Calculator (Lift ⊤) [] (λ _ → [])
 calculatorActor .force = receive ∞>>= λ {
-  (Msg Z (_ ∷ n ∷ m ∷ [])) .force → (Z ![t: Z ] ((lift (n + m)) ∷ [])) ∞>>
-    (strengthen [] >>
+  (Msg Z (tag ∷ _ ∷ n ∷ m ∷ [])) .force →
+    (Z ![t: Z ] ((lift tag) ∷ (lift (n + m)) ∷ [])) ∞>> (do
+    strengthen []
     calculatorActor)
   ; (Msg (S ()) _)
   }
 
 TestBox : InboxShape
-TestBox = ((ValueType ℕ ∷ [])) ∷ [] ∷ []
+TestBox = (
+  ValueType UniqueTag ∷
+  ValueType ℕ ∷ []) ∷
+  [] ∷ []
 
 calltestActor : ∀{i} → ∞ActorM i TestBox (Lift ℕ) [] (λ _ → [])
-calltestActor .force = spawn∞ calculatorActor ∞>>
-                       (call Z Z ((lift 10) ∷ ((lift 32) ∷ [])) (Z ∷ []) Z >>= λ x →
-                       strengthen [] >>
+calltestActor .force = spawn∞ calculatorActor ∞>> (do
+                       x ← call Z Z 0 ((lift 10) ∷ ((lift 32) ∷ [])) (Z ∷ []) Z
+                       strengthen []
                        return-result x)
   where
-    return-result : SelectedMessage {TestBox} (call-select (Z ∷ []) Z) → ∀ {i} → ∞ActorM i TestBox (Lift ℕ) [] (λ _ → [])
-    return-result record { msg = (Msg Z (px ∷ x₁)) } = return px
+    return-result : SelectedMessage {TestBox} (call-select 0 (Z ∷ []) Z) →
+                    ∀ {i} → ∞ActorM i TestBox (Lift ℕ) [] (λ _ → [])
+    return-result record { msg = (Msg Z (tag ∷ n ∷ [])) } = return n
     return-result record { msg = (Msg (S x) x₁) ; msg-ok = () }