diff --git a/src/Examples/Call.agda b/src/Examples/Call.agda
index fa8416f..8546c69 100644
--- a/src/Examples/Call.agda
+++ b/src/Examples/Call.agda
@@ -65,6 +65,6 @@ calltestActor .force = spawn∞ calculatorActor ∞>>
                        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₁)) ; right-msg = right-msg ; waiting = waiting } = return px
-    return-result record { msg = (Msg (S x) x₁) ; right-msg = () }
+    return-result record { msg = (Msg Z (px ∷ x₁)) } = return px
+    return-result record { msg = (Msg (S x) x₁) ; msg-ok = () }
 
diff --git a/src/Examples/SelectiveReceive.agda b/src/Examples/SelectiveReceive.agda
deleted file mode 100644
index 680de32..0000000
--- a/src/Examples/SelectiveReceive.agda
+++ /dev/null
@@ -1,174 +0,0 @@
-module Examples.SelectiveReceive where
-
-open import ActorMonad public
-open import Data.List using (List ; _∷_ ; [] ; _++_)
-open import Data.List.All using (All ; _∷_ ; [])
-open import Data.List.Properties using (++-assoc ; ++-identityʳ)
-open import Data.Bool using (Bool ; if_then_else_ ; false ; true)
-open import Data.Nat using (ℕ ; zero ; suc)
-open import Level using (Level ; Lift ; lift) renaming (zero to lzero ; suc to lsuc)
-open import Size using (Size ; ↑_)
-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)
-open import Data.Unit using (⊤ ; tt)
-
-waiting-refs : ∀ {IS} → (q : List (Message IS)) → ReferenceTypes
-waiting-refs [] = []
-waiting-refs (x ∷ q) = add-references (waiting-refs q) x
-
-record SplitList {a : Level} {A : Set a} (ls : List A) : Set (lsuc a) where
-  field
-    heads : List A
-    el : A
-    tails : List A
-    is-ls : (heads) ++ (el ∷ tails) ≡ ls
-
-data FoundInList {a : Level} {A : Set a} (ls : List A) (f : A → Bool) : Set (lsuc a) where
-  Found : (split : SplitList ls) → (f (SplitList.el split) ≡ true) → FoundInList ls f
-  Nothing : FoundInList ls f
-
-find-split : {a : Level} {A : Set a} (ls : List A) (f : A → Bool) → FoundInList ls f
-find-split [] f = Nothing
-find-split (x ∷ ls) f with (f x) | (inspect f x)
-... | false | p = add-x (find-split ls f)
-  where
-    add-x : FoundInList ls f → FoundInList (x ∷ ls) f
-    add-x (Found split x₁) = Found (record { heads = x ∷ heads split ; el = el split ; tails = tails split ; is-ls = cong (_∷_ x) (is-ls split) }) x₁
-      where open SplitList
-    add-x Nothing = Nothing
-... | true | [ eq ] = Found (record { heads = [] ; el = x ; tails = ls ; is-ls = refl }) eq
-
-⊆++ : {a : Level} {A : Set a} (xs ys zs : List A) → xs ⊆ zs → ys ⊆ zs → (xs ++ ys) ⊆ zs
-⊆++ _ ys zs [] q = q
-⊆++ _ ys zs (x₁ ∷ p) q = x₁ ∷ (⊆++ _ ys zs p q)
-
-∈-insert : ∀ {a} {A : Set a} (xs ys : List A) → (x : A) → x ∈ (ys ++ x ∷ xs)
-∈-insert xs [] x = Z
-∈-insert xs (x₁ ∷ ys) x = S (∈-insert xs ys x)
-
--- count down both the proof and the list
--- Result depends on which is shortest
-insert-one : ∀ {a} {A : Set a} {x₁ : A} (xs ys : List A) → (y : A) → x₁ ∈ (xs ++ ys) → x₁ ∈ (xs ++ y ∷ ys)
-insert-one [] ys y p = S p
-insert-one (x ∷ xs) ys y Z = Z
-insert-one (x ∷ xs) ys y (S p) = S (insert-one xs ys y p)
-
-⊆-insert : ∀ {a} {A : Set a} (xs ys zs : List A) → (x : A) → xs ⊆ (ys ++ zs) → xs ⊆ (ys ++ x ∷ zs)
-⊆-insert [] ys zs x p = []
-⊆-insert (x₁ ∷ xs) ys zs x (x₂ ∷ p) = insert-one ys zs x x₂ ∷ (⊆-insert xs ys zs x p)
-
-⊆-move : {a : Level} {A : Set a} (xs ys : List A) → (xs ++ ys) ⊆ (ys ++ xs)
-⊆-move [] ys rewrite (++-identityʳ ys) = ⊆-refl
-⊆-move (x ∷ xs) ys with (⊆-move xs ys)
-... | q = ∈-insert xs ys x ∷ ⊆-insert (xs ++ ys) ys xs x q
-
-⊆-skip : {a : Level} {A : Set a} (xs ys zs : List A) → ys ⊆ zs → (xs ++ ys) ⊆ (xs ++ zs)
-⊆-skip [] ys zs p = p
-⊆-skip (x ∷ xs) ys zs p = Z ∷ (⊆-suc (⊆-skip xs ys zs p))
-
-⊆++-refl : ∀ {a} {A : Set a} → (xs ys : List A) → xs ⊆ (xs ++ ys)
-⊆++-refl [] ys = []
-⊆++-refl (x ∷ xs) ys = Z ∷ (⊆-suc (⊆++-refl xs ys))
-
-⊆++-l-refl : ∀ {a} {A : Set a} → (xs ys : List A) → xs ⊆ (ys ++ xs)
-⊆++-l-refl xs [] = ⊆-refl
-⊆++-l-refl xs (x ∷ ys) = ⊆-suc (⊆++-l-refl xs ys)
-
-∈-inc : ∀ {a} {A : Set a} (xs ys : List A) → (x : A) → x ∈ xs → (x ∈ (xs ++ ys))
-∈-inc _ ys x Z = Z
-∈-inc _ ys x (S p) = S (∈-inc _ ys x p)
-
-⊆-inc : ∀ {a} {A : Set a} (xs ys zs : List A) → xs ⊆ ys → (xs ++ zs) ⊆ (ys ++ zs)
-⊆-inc [] [] zs p = ⊆-refl
-⊆-inc [] (x ∷ ys) zs p = ⊆++-l-refl zs (x ∷ ys)
-⊆-inc (x ∷ xs) ys zs (px ∷ p) = ∈-inc ys zs x px ∷ (⊆-inc xs ys zs p)
-
-⊆++comm : ∀ {a} {A : Set a} (xs ys zs : List A) → ((xs ++ ys) ++ zs) ⊆ (xs ++ (ys ++ zs))
-⊆++comm [] ys zs = ⊆-refl
-⊆++comm (x ∷ xs) ys zs = Z ∷ (⊆-suc (⊆++comm xs ys zs))
-
-⊆++comm' : ∀ {a} {A : Set a} (xs ys zs : List A) → (xs ++ ys ++ zs) ⊆ ((xs ++ ys) ++ zs)
-⊆++comm' [] ys zs = ⊆-refl
-⊆++comm' (x ∷ xs) ys zs = Z ∷ ⊆-suc (⊆++comm' xs ys zs)
-
-add-references++ : ∀ {IS} → (xs ys : ReferenceTypes) → (x : Message IS) → add-references (xs ++ ys) x ≡ add-references xs x ++ ys
-add-references++ xs ys (Msg {MT} x x₁) = sym (++-assoc (extract-references MT) xs ys)
-
-waiting-refs++ : ∀ {IS} → (xs ys : List (Message IS)) → waiting-refs (xs ++ ys) ≡ waiting-refs xs ++ waiting-refs ys
-waiting-refs++ [] _ = refl
-waiting-refs++ (x ∷ xs) ys with (waiting-refs++ xs ys)
-... | q with (cong (λ qs → add-references qs x) q)
-... | r = trans r (halp xs ys x)
-  where
-    halp : ∀ {IS} → (xs ys : List (Message IS)) (x : Message IS) →
-      add-references (waiting-refs xs ++ waiting-refs ys) x ≡
-      add-references (waiting-refs xs) x ++ waiting-refs ys
-    halp xs ys x = add-references++ (waiting-refs xs) (waiting-refs ys) x
-
-move-received : ∀ {IS} → ∀ pre → (q : List (Message IS)) → (x : Message IS) → ((pre ++ (waiting-refs (q ++ (x ∷ [])))) ⊆ (add-references (pre ++ waiting-refs q) x))
-move-received pre q (Msg {MT} x x₁) rewrite (waiting-refs++ q (Msg x x₁ ∷ [])) | (++-identityʳ (extract-references MT)) = ⊆-trans move-1 move-2
-  where
-    move-1 : (pre ++ waiting-refs q ++ extract-references MT) ⊆ ((pre ++ waiting-refs q) ++ extract-references MT)
-    move-1 = ⊆++comm' pre (waiting-refs q) (extract-references MT)
-    move-2 : ((pre ++ waiting-refs q) ++ extract-references MT) ⊆ (extract-references MT ++ (pre ++ waiting-refs q))
-    move-2 = ⊆-move (pre ++ waiting-refs q) (extract-references MT)
-
-accept-received : ∀ {IS} → ∀ pre → (q : List (Message IS)) → (x : Message IS) →  (add-references pre x ++ waiting-refs q) ⊆ (add-references (pre ++ waiting-refs q) x)
-accept-received pre q (Msg {MT} x x₁) = ⊆++comm (extract-references MT) pre (waiting-refs q)
-
-open SplitList
-
-
-accept-found : ∀ {IS} → ∀ pre → (q : List (Message IS)) → (split : SplitList q) →
-               (add-references pre (el split) ++ waiting-refs (heads split ++ tails split)) ⊆ (pre ++ waiting-refs q)
-accept-found pre q record { heads = heads ; el = Msg {MT} x y ; tails = tails ; is-ls = is-ls } rewrite (sym is-ls) =
-  ⊆-trans (⊆-inc (extract-references MT ++ pre) (pre ++ extract-references MT) (waiting-refs (heads ++ tails)) (⊆-move (extract-references MT) pre))
-  (⊆-trans (⊆++comm pre (extract-references MT) (waiting-refs (heads ++ tails)))
-  (⊆-skip pre (extract-references MT ++ waiting-refs (heads ++ tails)) (waiting-refs (heads ++ Msg x y ∷ tails))
-  final-move))
-  where
-    final-move : (extract-references MT ++ waiting-refs (heads ++ tails)) ⊆ waiting-refs (heads ++ Msg x y ∷ tails)
-    final-move rewrite (waiting-refs++ heads tails) | (waiting-refs++ heads (Msg x y ∷ tails)) = ⊆-trans (⊆++comm' (extract-references MT) (waiting-refs heads) (waiting-refs tails))
-      (⊆-trans (⊆-inc (extract-references MT ++ waiting-refs heads) (waiting-refs heads ++ extract-references MT) (waiting-refs tails)
-        (⊆-move (extract-references MT) (waiting-refs heads)))
-      (⊆++comm (waiting-refs heads) (extract-references MT) (waiting-refs tails)))
-
-record SelRec (IS : InboxShape) (f : Message IS → Bool) : Set₁ where
-  field
-    msg : Message IS
-    right-msg : f msg ≡ true
-    waiting : List (Message IS)
-
-open SelRec
-
-selective-receive : ∀ {i IS pre} → (q : List (Message IS)) → (f : Message IS → Bool) → ∞ActorM i IS (SelRec IS f) (pre ++ (waiting-refs q)) (λ m → (add-references pre (msg m)) ++ (waiting-refs (waiting m)))
-selective-receive {IS = IS} {pre} q f = case-of-find (find-split q f)
-  where
-    case-of-find : ∀ {i} → FoundInList q f → ∞ActorM i IS (SelRec IS f) (pre ++ waiting-refs q) (λ m → add-references pre (msg m) ++ waiting-refs (waiting m))
-    case-of-find (Found split x) .force = strengthen (accept-found pre q split) ∞>> return₁ (record { msg = el split ; right-msg = x ; waiting = (heads split) ++ (tails split) })
-    case-of-find Nothing .force = receive ∞>>= handle-receive
-      where
-        handle-receive : ∀ {i} (x : Message IS) → ∞ActorM i IS (SelRec IS f) (add-references (pre ++ waiting-refs q) x) (λ m → (add-references pre (msg m) ++ waiting-refs (waiting m)))
-        handle-receive x with (f x) | (inspect f x)
-        handle-receive {i} x  | false | p = strengthen (move-received pre q x) >> selective-receive (q ++ (x ∷ [])) f
-        handle-receive x | true | [ p ] = strengthen (accept-received pre q x) >> return₁ ret-v
-          where
-            ret-v : SelRec IS f
-            ret-v = record { msg = x ; right-msg = p ; waiting = q }
-
-SelectiveTestBox : InboxShape
-SelectiveTestBox = (ValueType Bool ∷ []) ∷ []
-
-testActor : ∀ {i} → ActorM i SelectiveTestBox (Lift Bool) [] (λ _ → [])
-testActor = selective-receive [] only-true ∞>>= after-receive
-  where
-    only-true : Message SelectiveTestBox → Bool
-    only-true (Msg Z (b ∷ [])) = b
-    only-true (Msg (S ()) x₁)
-    after-receive : ∀ {i} (x : SelRec SelectiveTestBox only-true) → ∞ActorM i SelectiveTestBox (Lift Bool) (add-references [] (msg x) ++ waiting-refs (waiting x)) (λ _ → [])
-    after-receive record { msg = (Msg Z (.true ∷ [])) ; right-msg = refl ; waiting = waiting } = strengthen [] >> return true
-    after-receive record { msg = (Msg (S ()) x₁) ; right-msg = right-msg ; waiting = waiting }
-
-spawner : ∀ {i} → ActorM i [] ⊤₁ [] (λ _ → [])
-spawner = spawn testActor ∞>> ((Z ![t: Z ] ((lift false) ∷ [])) >> strengthen [])
diff --git a/src/Examples/SelectiveReceive.lagda.tex b/src/Examples/SelectiveReceive.lagda.tex
new file mode 100644
index 0000000..cc54805
--- /dev/null
+++ b/src/Examples/SelectiveReceive.lagda.tex
@@ -0,0 +1,351 @@
+\begin{code}
+
+module Examples.SelectiveReceive where
+
+open import ActorMonad public
+open import Data.List using (List ; _∷_ ; [] ; _++_)
+open import Data.List.All using (All ; _∷_ ; [])
+open import Data.List.Properties using (++-assoc ; ++-identityʳ)
+open import Data.Bool using (Bool ; false ; true)
+open import Data.Nat using (ℕ ; zero ; suc)
+open import Level using (Level ; Lift ; lift)
+            renaming (zero to lzero ; suc to lsuc)
+open import Size using (Size ; ↑_)
+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)
+open import Data.Unit using (⊤ ; tt)
+
+
+waiting-refs : ∀ {IS} → (q : List (Message IS)) → ReferenceTypes
+waiting-refs [] = []
+waiting-refs (x ∷ q) = add-references (waiting-refs q) x
+
+record SplitList {a : Level} {A : Set a} (ls : List A) : Set (lsuc a) where
+  field
+    heads : List A
+    el : A
+    tails : List A
+    is-ls : (heads) ++ (el ∷ tails) ≡ ls
+
+data FoundInList {a : Level} {A : Set a}
+                 (ls : List A) (f : A → Bool) : Set (lsuc a) where
+  Found : (split : SplitList ls) →
+          (f (SplitList.el split) ≡ true) →
+          FoundInList ls f
+  Nothing : FoundInList ls f
+
+find-split : {a : Level} {A : Set a}
+             (ls : List A) (f : A → Bool) →
+             FoundInList ls f
+find-split [] f = Nothing
+find-split (x ∷ ls) f with (f x) | (inspect f x)
+... | false | p = add-x (find-split ls f)
+  where
+    add-x : FoundInList ls f → FoundInList (x ∷ ls) f
+    add-x (Found split el-is-ok) = Found (record {
+      heads = x ∷ heads split
+      ; el = el split
+      ; tails = tails split
+      ; is-ls = cong (_∷_ x) (is-ls split)
+      }) el-is-ok
+      where open SplitList
+    add-x Nothing = Nothing
+... | true | [ eq ] = Found (record {
+      heads = []
+      ; el = x
+      ; tails = ls
+      ; is-ls = refl
+      }) eq
+
+⊆++ : {a : Level} {A : Set a}
+      (xs ys zs : List A) →
+      xs ⊆ zs → ys ⊆ zs →
+      (xs ++ ys) ⊆ zs
+⊆++ _ ys zs [] q = q
+⊆++ _ ys zs (x₁ ∷ p) q = x₁ ∷ (⊆++ _ ys zs p q)
+
+∈-insert : ∀ {a} {A : Set a}
+           (xs ys : List A) →
+           (x : A) →
+           x ∈ (ys ++ x ∷ xs)
+∈-insert xs [] x = Z
+∈-insert xs (x₁ ∷ ys) x = S (∈-insert xs ys x)
+
+-- count down both the proof and the list
+-- Result depends on which is shortest
+insert-one : ∀ {a} {A : Set a} {x₁ : A}
+               (xs ys : List A) →
+               (y : A) →
+               x₁ ∈ (xs ++ ys) →
+               x₁ ∈ (xs ++ y ∷ ys)
+insert-one [] ys y p = S p
+insert-one (x ∷ xs) ys y Z = Z
+insert-one (x ∷ xs) ys y (S p) = S (insert-one xs ys y p)
+
+⊆-insert : ∀ {a} {A : Set a}
+                 (xs ys zs : List A) →
+                 (x : A) →
+                 xs ⊆ (ys ++ zs) →
+                 xs ⊆ (ys ++ x ∷ zs)
+⊆-insert [] ys zs x p = []
+⊆-insert (x₁ ∷ xs) ys zs x (x₂ ∷ p) = insert-one ys zs x x₂ ∷
+                                                 (⊆-insert xs ys zs x p)
+
+⊆-move : {a : Level} {A : Set a}
+                     (xs ys : List A) →
+                     (xs ++ ys) ⊆ (ys ++ xs)
+⊆-move [] ys rewrite (++-identityʳ ys) = ⊆-refl
+⊆-move (x ∷ xs) ys with (⊆-move xs ys)
+... | q = ∈-insert xs ys x ∷ ⊆-insert (xs ++ ys) ys xs x q
+
+⊆-skip : {a : Level} {A : Set a}
+         (xs ys zs : List A) →
+         ys ⊆ zs →
+         (xs ++ ys) ⊆ (xs ++ zs)
+⊆-skip [] ys zs p = p
+⊆-skip (x ∷ xs) ys zs p = Z ∷ (⊆-suc (⊆-skip xs ys zs p))
+
+⊆++-refl : ∀ {a} {A : Set a} →
+           (xs ys : List A) →
+           xs ⊆ (xs ++ ys)
+⊆++-refl [] ys = []
+⊆++-refl (x ∷ xs) ys = Z ∷ (⊆-suc (⊆++-refl xs ys))
+
+⊆++-l-refl : ∀ {a} {A : Set a} →
+                   (xs ys : List A) →
+                   xs ⊆ (ys ++ xs)
+⊆++-l-refl xs [] = ⊆-refl
+⊆++-l-refl xs (x ∷ ys) = ⊆-suc (⊆++-l-refl xs ys)
+
+∈-inc : ∀ {a} {A : Set a}
+              (xs ys : List A) →
+              (x : A) →
+              x ∈ xs →
+              x ∈ (xs ++ ys)
+∈-inc _ ys x Z = Z
+∈-inc _ ys x (S p) = S (∈-inc _ ys x p)
+
+⊆-inc : ∀ {a} {A : Set a}
+              (xs ys zs : List A) →
+              xs ⊆ ys →
+              (xs ++ zs) ⊆ (ys ++ zs)
+⊆-inc [] [] zs p = ⊆-refl
+⊆-inc [] (x ∷ ys) zs p = ⊆++-l-refl zs (x ∷ ys)
+⊆-inc (x ∷ xs) ys zs (px ∷ p) = ∈-inc ys zs x px ∷ (⊆-inc xs ys zs p)
+
+⊆++comm : ∀ {a} {A : Set a}
+            (xs ys zs : List A) →
+            ((xs ++ ys) ++ zs) ⊆ (xs ++ (ys ++ zs))
+⊆++comm [] ys zs = ⊆-refl
+⊆++comm (x ∷ xs) ys zs = Z ∷ (⊆-suc (⊆++comm xs ys zs))
+
+⊆++comm' : ∀ {a} {A : Set a}
+           (xs ys zs : List A) →
+           (xs ++ ys ++ zs) ⊆ ((xs ++ ys) ++ zs)
+⊆++comm' [] ys zs = ⊆-refl
+⊆++comm' (x ∷ xs) ys zs = Z ∷ ⊆-suc (⊆++comm' xs ys zs)
+
+add-references++ : ∀ {IS} → (xs ys : ReferenceTypes) →
+                   (x : Message IS) →
+                     add-references (xs ++ ys) x ≡
+                     add-references xs x ++ ys
+add-references++ xs ys (Msg {MT} x x₁) =
+                 sym (++-assoc (extract-references MT) xs ys)
+
+waiting-refs++ : ∀ {IS} → (xs ys : List (Message IS)) →
+                        waiting-refs (xs ++ ys) ≡
+                        waiting-refs xs ++ waiting-refs ys
+waiting-refs++ [] _ = refl
+waiting-refs++ (x ∷ xs) ys with (waiting-refs++ xs ys)
+... | q with (cong (λ qs → add-references qs x) q)
+... | r = trans r (halp xs ys x)
+  where
+    halp : ∀ {IS} → (xs ys : List (Message IS)) (x : Message IS) →
+      add-references (waiting-refs xs ++ waiting-refs ys) x ≡
+      add-references (waiting-refs xs) x ++ waiting-refs ys
+    halp xs ys x = add-references++ (waiting-refs xs) (waiting-refs ys) x
+
+move-received : ∀ {IS} → ∀ pre →
+                (q : List (Message IS)) →
+                (x : Message IS) →
+                  (pre ++ (waiting-refs (q ++ (x ∷ [])))) ⊆
+                  (add-references (pre ++ waiting-refs q) x)
+move-received pre q (Msg {MT} x x₁) rewrite
+                    (waiting-refs++ q (Msg x x₁ ∷ [])) |
+                    (++-identityʳ (extract-references MT)) =
+                    ⊆-trans move-1 move-2
+  where
+    move-1 : (pre ++ waiting-refs q ++ extract-references MT) ⊆
+             ((pre ++ waiting-refs q) ++ extract-references MT)
+    move-1 = ⊆++comm' pre (waiting-refs q) (extract-references MT)
+    move-2 : ((pre ++ waiting-refs q) ++ extract-references MT) ⊆
+             (extract-references MT ++ (pre ++ waiting-refs q))
+    move-2 = ⊆-move (pre ++ waiting-refs q) (extract-references MT)
+
+accept-received : ∀ {IS} → ∀ pre →
+                  (q : List (Message IS)) →
+                  (x : Message IS) →
+                    (add-references pre x ++ waiting-refs q) ⊆
+                    (add-references (pre ++ waiting-refs q) x)
+accept-received pre q (Msg {MT} x x₁) = ⊆++comm
+                                        (extract-references MT)
+                                        pre
+                                        (waiting-refs q)
+
+open SplitList
+
+
+accept-found : ∀ {IS} → ∀ Γ →
+               (q : List (Message IS)) →
+               (split : SplitList q) →
+                 (add-references Γ (el split) ++
+                   waiting-refs (heads split ++ tails split)) ⊆
+                 (Γ ++ waiting-refs q)
+accept-found Γ q record {
+  heads = heads
+  ; el = Msg {MT} x y
+  ; tails = tails
+  ; is-ls = is-ls
+  } rewrite (sym is-ls) =
+  ⊆-trans
+    (⊆-inc
+      (extract-references MT ++ Γ)
+      (Γ ++ extract-references MT)
+      (waiting-refs (heads ++ tails))
+      (⊆-move (extract-references MT) Γ)
+    )
+    (⊆-trans
+      (⊆++comm
+        Γ
+        (extract-references MT)
+        (waiting-refs (heads ++ tails))
+      )
+      (⊆-skip
+        Γ
+        (extract-references MT ++ waiting-refs (heads ++ tails))
+        (waiting-refs (heads ++ Msg x y ∷ tails))
+        final-move
+      )
+    )
+  where
+    final-move : (extract-references MT ++ waiting-refs (heads ++ tails)) ⊆
+                 waiting-refs (heads ++ Msg x y ∷ tails)
+    final-move rewrite
+      (waiting-refs++ heads tails) |
+      (waiting-refs++ heads (Msg x y ∷ tails)) =
+      ⊆-trans
+        (⊆++comm'
+          (extract-references MT)
+          (waiting-refs heads)
+          (waiting-refs tails)
+        )
+        (⊆-trans
+          (⊆-inc
+            (extract-references MT ++ waiting-refs heads)
+            (waiting-refs heads ++ extract-references MT)
+            (waiting-refs tails)
+            (⊆-move (extract-references MT) (waiting-refs heads))
+          )
+          (⊆++comm
+            (waiting-refs heads)
+            (extract-references MT)
+            (waiting-refs tails)
+          )
+        )
+
+MessageFilter : (IS : InboxShape) → Set₁
+MessageFilter IS = Message IS → Bool
+\end{code}
+%<*SelRec>
+\begin{code}
+record SelRec (IS : InboxShape) (f : MessageFilter IS) : Set₁ where
+  field
+    msg : Message IS
+    msg-ok : f msg ≡ true
+    waiting : List (Message IS)
+\end{code}
+%</SelRec>
+\begin{code}
+open SelRec
+\end{code}
+%<*selective-receive>
+\begin{code}
+selective-receive : ∀ {i IS Γ} →
+                      (q : List (Message IS)) →
+                      (f : MessageFilter IS) →
+                      ∞ActorM i IS
+                        (SelRec IS f)
+                        (Γ ++ (waiting-refs q))
+                        (λ m → add-references Γ (msg m) ++
+                               waiting-refs (waiting m))
+\end{code}
+%</selective-receive>
+\begin{code}
+selective-receive {IS = IS} {Γ} q f = case-of-find (find-split q f)
+  where
+    case-of-find : ∀ {i} →
+                     FoundInList q f →
+                     ∞ActorM i IS
+                       (SelRec IS f)
+                       (Γ ++ waiting-refs q)
+                       (λ m → add-references Γ (msg m) ++
+                              waiting-refs (waiting m))
+    case-of-find (Found split x) .force =
+      strengthen (accept-found Γ q split) ∞>>
+      return₁ (record {
+        msg = el split
+        ; msg-ok = x
+        ; waiting = (heads split) ++ (tails split)
+        })
+    case-of-find Nothing .force =
+      receive ∞>>=
+      handle-receive
+      where
+        handle-receive : ∀ {i}
+                           (x : Message IS) →
+                           ∞ActorM i IS
+                             (SelRec IS f)
+                             (add-references (Γ ++ waiting-refs q) x)
+                             (λ m → add-references Γ (msg m) ++
+                                    waiting-refs (waiting m))
+        handle-receive x with (f x) | (inspect f x)
+        handle-receive {i} x  | false | p =
+          strengthen (move-received Γ q x) >>
+          selective-receive (q ++ (x ∷ [])) f
+        handle-receive x | true | [ p ] =
+          strengthen (accept-received Γ q x) >>
+          return₁ ret-v
+          where
+            ret-v : SelRec IS f
+            ret-v = record { msg = x ; msg-ok = p ; waiting = q }
+\end{code}
+
+\begin{code}
+SelectiveTestBox : InboxShape
+SelectiveTestBox = (ValueType Bool ∷ []) ∷ []
+
+testActor : ∀ {i} → ActorM i SelectiveTestBox (Lift Bool) [] (λ _ → [])
+testActor = selective-receive [] only-true ∞>>= after-receive
+  where
+    only-true : Message SelectiveTestBox → Bool
+    only-true (Msg Z (b ∷ [])) = b
+    only-true (Msg (S ()) x₁)
+    after-receive : ∀ {i}
+                    (x : SelRec SelectiveTestBox only-true) →
+                    ∞ActorM i SelectiveTestBox (Lift Bool)
+                      (add-references [] (msg x) ++ waiting-refs (waiting x))
+                      (λ _ → [])
+    after-receive record { msg = (Msg Z (.true ∷ [])) ; msg-ok = refl } =
+      strengthen [] >>
+      return true
+    after-receive record { msg = (Msg (S ()) _) }
+
+spawner : ∀ {i} → ActorM i [] ⊤₁ [] (λ _ → [])
+spawner =
+  spawn testActor ∞>>
+  ((Z ![t: Z ] ((lift false) ∷ [])) >>
+  strengthen [])
+\end{code}
diff --git a/src/Selective/ActorMonad.lagda.tex b/src/Selective/ActorMonad.lagda.tex
index 06b7dc0..81a7f47 100644
--- a/src/Selective/ActorMonad.lagda.tex
+++ b/src/Selective/ActorMonad.lagda.tex
@@ -117,6 +117,7 @@
     Receive : ∀ {pre} → ActorM i IS (Message IS) pre (add-references pre)
 \end{code}
 %<*SelectiveReceiveConstruct>
+\AgdaTarget{SelectiveReceive}
 \begin{code}
     SelectiveReceive : ∀ {pre} → (filter : MessageFilter IS) →
       ActorM i IS (SelectedMessage filter) pre (add-selected-references pre)
@@ -185,22 +186,22 @@
     (canSendTo : ToIS ∈ pre) →
     (MT ∈ ToIS) →
     All (send-field-content pre) MT →
-    ∞ActorM i IS ⊤₁ pre (λ _ → pre)
+    ∞ActorM (↑ i) IS ⊤₁ pre (λ _ → pre)
 (canSendTo ![t: p ] fields) .force = Send canSendTo (SendM p fields)
 
 -- coinduction helper for Receive
-receive : ∀ {i IS pre} → ∞ActorM i IS (Message IS) pre (add-references pre)
+receive : ∀ {i IS pre} → ∞ActorM (↑ i) IS (Message IS) pre (add-references pre)
 receive .force = Receive
 
 selective-receive : ∀ {i IS pre} → (filter : MessageFilter IS) →
-  ∞ActorM i IS (SelectedMessage filter) pre (add-selected-references pre)
+  ∞ActorM (↑ i) IS (SelectedMessage filter) pre (add-selected-references pre)
 selective-receive filter .force = SelectiveReceive filter
 
-self : ∀ {i IS pre} → ∞ActorM i IS ⊤₁ pre (λ _ → IS ∷ pre)
+self : ∀ {i IS pre} → ∞ActorM (↑ i) IS ⊤₁ pre (λ _ → IS ∷ pre)
 self .force = Self
 
 -- coinduction helper for Strengthen
-strengthen : ∀ {i IS xs ys} → ys ⊆ xs → ∞ActorM i IS ⊤₁ xs (λ _ → ys)
+strengthen : ∀ {i IS xs ys} → ys ⊆ xs → ∞ActorM (↑ i) IS ⊤₁ xs (λ _ → ys)
 strengthen inc .force = Strengthen inc
 
 ⊠-of-values : List Set → InboxShape