diff --git a/theories/.gitignore b/theories/.gitignore
index 059a8ee..4adf2fb 100644
--- a/theories/.gitignore
+++ b/theories/.gitignore
@@ -21,6 +21,7 @@
 *.vo
 *.vok
 *.vos
+.coq-native
 .rocq-native
 .csdp.cache
 .lia.cache
diff --git a/theories/Lang/Yield.v b/theories/Lang/Yield.v
new file mode 100644
index 0000000..adc1084
--- /dev/null
+++ b/theories/Lang/Yield.v
@@ -0,0 +1,10 @@
+From TICL Require Export
+  Lang.Yield.Events
+  Lang.Yield.Syntax
+  Lang.Yield.Vec
+  Lang.Yield.Denote
+  Lang.Yield.Scheduler
+  Lang.Yield.Interp
+  Lang.Yield.Ticl
+  Lang.Yield.SBisim
+  Lang.Yield.SchedulerFairness.
diff --git a/theories/Lang/Yield/Denote.v b/theories/Lang/Yield/Denote.v
new file mode 100644
index 0000000..08a4108
--- /dev/null
+++ b/theories/Lang/Yield/Denote.v
@@ -0,0 +1,110 @@
+From Stdlib Require Import Nat Strings.String.
+From ExtLib Require Import Data.Map.FMapAList Data.String Structures.Maps.
+From TICL Require Import
+  ICTree.Core
+  Events.StateE
+  Lang.Maps
+  Lang.Yield.Events
+  Lang.Yield.Syntax.
+
+Import ICtree ICTreeNotations.
+Local Open Scope ictree_scope.
+
+Definition Ctx := alist string nat.
+Definition Mem := stateE Ctx.
+
+(** Raw Yield denotations can yield, fork, and access memory. *)
+Definition YEff := yieldE + (forkE + Mem).
+
+Definition ytrigger (e : YEff) : ictree YEff (encode e) :=
+  @ICtree.trigger YEff YEff _ _ ReSum_refl ReSumRet_refl e.
+Definition yget : ictree YEff Ctx := ytrigger (inr (inr Get)).
+Definition yput (m : Ctx) : ictree YEff unit :=
+  ytrigger (inr (inr (Put m))).
+Definition yyield : ictree YEff unit := ytrigger (inl Yield).
+Definition yfork : ictree YEff bool := ytrigger (inr (inl Fork)).
+
+(** Denotation of expressions.  Successful variable reads yield once before
+    returning the value; missing variables remain stuck. *)
+Fixpoint denote_exp (e : YExp) : ictree YEff nat :=
+  match e with
+  | YVar name =>
+      ctx <- yget;;
+      match lookup name ctx with
+      | Some value => yyield;; Ret value
+      | None => stuck
+      end
+  | YLit n => Ret n
+  | YPlus a b =>
+      x <- denote_exp a;;
+      y <- denote_exp b;;
+      Ret (x + y)%nat
+  | YMinus a b =>
+      x <- denote_exp a;;
+      y <- denote_exp b;;
+      Ret (x - y)%nat
+  | YMult a b =>
+      x <- denote_exp a;;
+      y <- denote_exp b;;
+      Ret (x * y)%nat
+  end.
+
+(** Internal result used to prevent child threads from inheriting source
+    continuations outside their fork body.
+
+    [Fallthrough] means the current thread should continue with the enclosing
+    source continuation.  [HaltThread] means a spawned child has finished its
+    declared body and must not inherit enclosing continuations. *)
+Inductive YStmtFlow : Type :=
+| Fallthrough
+| HaltThread.
+
+(** Flow-sensitive denotation of statements. *)
+Fixpoint denote_stmt_flow (s : YStmt) : ictree YEff YStmtFlow :=
+  match s with
+  | YAssign name expr =>
+      value <- denote_exp expr;;
+      ctx <- yget;;
+      yput (add name value ctx);;
+      Ret Fallthrough
+  | YSeq a b =>
+      flow <- denote_stmt_flow a;;
+      match flow with
+      | Fallthrough => denote_stmt_flow b
+      | HaltThread => Ret HaltThread
+      end
+  | YIf test then_branch else_branch =>
+      condition_value <- denote_exp test;;
+      if is_true condition_value then
+        denote_stmt_flow then_branch
+      else
+        denote_stmt_flow else_branch
+  | YWhile test body =>
+      ICtree.iter
+        (fun _ =>
+           condition_value <- denote_exp test;;
+           if is_true condition_value then
+             flow <- denote_stmt_flow body;;
+             match flow with
+             | Fallthrough => Ret (inl tt)
+             | HaltThread => Ret (inr HaltThread)
+             end
+           else
+             Ret (inr Fallthrough)) tt
+  | YFork body =>
+      in_child <- yfork;;
+      if in_child then
+        _ <- denote_stmt_flow body;;
+        Ret HaltThread
+      else
+        Ret Fallthrough
+  | YSkip => Ret Fallthrough
+  | YYield =>
+      yyield;;
+      Ret Fallthrough
+  end.
+
+(** Public denotation of statements to unscheduled Yield threads. *)
+Definition denote_stmt (s : YStmt) : ictree YEff unit :=
+  _ <- denote_stmt_flow s;;
+  Ret tt.
diff --git a/theories/Lang/Yield/Events.v b/theories/Lang/Yield/Events.v
new file mode 100644
index 0000000..2b6ddb1
--- /dev/null
+++ b/theories/Lang/Yield/Events.v
@@ -0,0 +1,40 @@
+From Stdlib Require Import Fin.
+From TICL Require Import ICTree.Core Events.Core.
+
+Generalizable All Variables.
+
+(** Cooperative scheduling point emitted by source-level [yield]. *)
+Variant yieldE : Type := Yield.
+
+(** Thread-local fork choice.  The scheduler interprets the resulting [bool]
+    to run both continuations. *)
+Variant forkE : Type := Fork.
+
+(** Scheduler-level observation that a fork spawned another runnable thread. *)
+Variant spawnE : Type := Spawn.
+
+#[global] Instance Encode_yieldE : Encode yieldE :=
+  fun e => match e with Yield => unit end.
+#[global] Instance Encode_forkE : Encode forkE :=
+  fun e => match e with Fork => bool end.
+#[global] Instance Encode_spawnE : Encode spawnE :=
+  fun e => match e with Spawn => unit end.
+
+Definition yield {E} `{HE : Encode E} `{RS : ReSum yieldE E}
+           `{RR : @ReSumRet yieldE E Encode_yieldE HE RS} : ictree E unit :=
+  @ICtree.trigger yieldE E Encode_yieldE HE RS RR Yield.
+Definition fork {E} `{HE : Encode E} `{RS : ReSum forkE E}
+           `{RR : @ReSumRet forkE E Encode_forkE HE RS} : ictree E bool :=
+  @ICtree.trigger forkE E Encode_forkE HE RS RR Fork.
+Definition spawn {E} `{HE : Encode E} `{RS : ReSum spawnE E}
+           `{RR : @ReSumRet spawnE E Encode_spawnE HE RS} : ictree E unit :=
+  @ICtree.trigger spawnE E Encode_spawnE HE RS RR Spawn.
+
+(** A runnable source thread may yield, fork, or perform user effects. *)
+Definition thread (E : Type) `{Encode E} := ictree (yieldE + (forkE + E)) unit.
+
+(** A scheduled computation exposes yields and spawns, but no raw forks. *)
+Definition completed (E : Type) `{Encode E} := ictree (yieldE + (spawnE + E)) unit.
+
+(** Finite thread pools are represented as functions from finite indices. *)
+Definition pool (E : Type) `{Encode E} (n : nat) := Fin.t n -> thread E.
diff --git a/theories/Lang/Yield/Interp.v b/theories/Lang/Yield/Interp.v
new file mode 100644
index 0000000..14c4e9e
--- /dev/null
+++ b/theories/Lang/Yield/Interp.v
@@ -0,0 +1,92 @@
+From Stdlib Require Import Fin.
+From ExtLib Require Import
+  Structures.Monad
+  Data.Monads.StateMonad
+  Structures.MonadState
+  Data.Map.FMapAList
+  Data.String.
+From TICL Require Import
+  ICTree.Core
+  ICTree.Interp.Core
+  ICTree.Interp.State
+  ICTree.Events.State
+  ICTree.Events.Writer
+  Events.Core
+  Events.StateE
+  Lang.Maps
+  Lang.Yield.Events
+  Lang.Yield.Syntax
+  Lang.Yield.Denote
+  Lang.Yield.Scheduler.
+
+Import ICtree ICTreeNotations.
+Local Open Scope ictree_scope.
+
+(** Start a source statement as a singleton pool focused on its only thread.
+    This is the scheduler-visible view: source [Fork] events have been
+    scheduled into scheduler [Spawn] observations, and cooperative [Yield]
+    observations remain visible alongside memory effects. *)
+Definition scheduled_visible (s : YStmt) : completed Mem :=
+  schedule 1 (fun _ => denote_stmt s) (Some Fin.F1).
+
+(** Backward-compatible name for the scheduler-visible scheduled computation. *)
+Definition scheduled : YStmt -> completed Mem := scheduled_visible.
+
+(** Erase scheduler spawn observations while preserving yield and memory events. *)
+Definition handle_spawn : (yieldE + (spawnE + Mem)) ~> ictree (yieldE + Mem) :=
+  fun event =>
+    match event with
+    | inl y => ICtree.trigger y
+    | inr (inl Spawn) => Ret tt
+    | inr (inr m) => ICtree.trigger m
+    end.
+Definition interp_spawn {X} (t : ictree (yieldE + (spawnE + Mem)) X) : ictree (yieldE + Mem) X :=
+  interp handle_spawn t.
+
+(** Erase cooperative yield observations, leaving only memory effects. *)
+Definition handle_yield : (yieldE + Mem) ~> ictree Mem :=
+  fun event =>
+    match event with
+    | inl Yield => Ret tt
+    | inr m => ICtree.trigger m
+    end.
+Definition interp_yield {X} (t : ictree (yieldE + Mem) X) : ictree Mem X :=
+  interp handle_yield t.
+
+(** Erased scheduled interpretation: both scheduler [Spawn] and cooperative
+    [Yield] observations are intentionally erased, leaving only memory effects. *)
+Definition interp_scheduled_erased (s : YStmt) : ictree Mem unit :=
+  interp_yield (interp_spawn (scheduled_visible s)).
+
+(** Backward-compatible erased scheduled interpretation.  New concurrency-facing
+    code should choose explicitly between [scheduled_visible] and
+    [interp_scheduled_erased]. *)
+Definition interp_scheduled : YStmt -> ictree Mem unit := interp_scheduled_erased.
+
+(** Interpret a raw thread without scheduling by resolving [Fork] to [false],
+    so a standalone thread behaves as the parent path and never starts the
+    fork body. *)
+Definition handle_thread : YEff ~> ictree (yieldE + Mem) :=
+  fun event =>
+    match event with
+    | inl y => ICtree.trigger y
+    | inr (inl Fork) => Ret false
+    | inr (inr m) => ICtree.trigger m
+    end.
+Definition interp_thread {X} (t : ictree YEff X) : ictree Mem X :=
+  interp_yield (interp handle_thread t).
+
+(** Erased expression instrumentation: raw thread-level [Yield] observations
+    are erased before state instrumentation. *)
+Definition instr_exp_erased (e : YExp) (ctx : Ctx) : ictreeW Ctx (nat * Ctx) :=
+  instr_stateE (interp_thread (denote_exp e)) ctx.
+
+(** Erased statement instrumentation: scheduler [Spawn] and cooperative [Yield]
+    observations are erased before state instrumentation. *)
+Definition instr_stmt_erased (s : YStmt) (ctx : Ctx) : ictreeW Ctx (unit * Ctx) :=
+  instr_stateE (interp_scheduled_erased s) ctx.
+
+(** Backward-compatible erased instrumentation aliases.  These names preserve the
+    iteration-1 API, where instrumentation observed only memory/state effects. *)
+Definition instr_exp : YExp -> Ctx -> ictreeW Ctx (nat * Ctx) := instr_exp_erased.
+Definition instr_stmt : YStmt -> Ctx -> ictreeW Ctx (unit * Ctx) := instr_stmt_erased.
diff --git a/theories/Lang/Yield/SBisim.v b/theories/Lang/Yield/SBisim.v
new file mode 100644
index 0000000..ee3f059
--- /dev/null
+++ b/theories/Lang/Yield/SBisim.v
@@ -0,0 +1,954 @@
+From Stdlib Require Import Fin Program.Equality.
+From TICL Require Import
+  ICTree.Core
+  ICTree.Trans
+  ICTree.Equ
+  ICTree.Eq.Core
+  ICTree.Eq.Bind
+  ICTree.SBisim
+  Lang.Yield.Events
+  Lang.Yield.Vec
+  Lang.Yield.Scheduler
+  Lang.Yield.Denote
+  Lang.Yield.Interp
+  Lang.Yield.Ticl.
+
+Import ICtree ICTreeNotations.
+Local Open Scope ictree_scope.
+
+Section PoolSBisim.
+  Context {E : Type} `{Encode E}.
+
+  Definition pool_sbisim {n : nat} (v1 v2 : pool E n) : Prop :=
+    forall i, v1 i ~ v2 i.
+
+  Lemma pool_sbisim_refl {n} (v : pool E n) : pool_sbisim v v.
+  Proof. intro i; reflexivity. Qed.
+
+  Lemma pool_sbisim_sym {n} (v1 v2 : pool E n) :
+    pool_sbisim v1 v2 -> pool_sbisim v2 v1.
+  Proof. intros Hpool i; symmetry; apply Hpool. Qed.
+
+  Lemma replace_pool_sbisim {n} (v1 v2 : pool E n) (i : Fin.t n)
+        (t1 t2 : thread E) :
+    pool_sbisim v1 v2 ->
+    t1 ~ t2 ->
+    pool_sbisim (replace_pool v1 i t1) (replace_pool v2 i t2).
+  Proof.
+    intros Hv Ht j.
+    unfold replace_pool.
+    destruct (Fin.eq_dec i j); auto.
+  Qed.
+
+  Lemma remove_pool_sbisim {n} (v1 v2 : pool E (S n)) (i : Fin.t (S n)) :
+    pool_sbisim v1 v2 ->
+    pool_sbisim (remove_pool v1 i) (remove_pool v2 i).
+  Proof.
+    intros Hv j.
+    revert v1 v2 i j Hv.
+    induction n as [| n IH]; intros v1 v2 i j Hv.
+    - dependent destruction j.
+    - cbn.
+      dependent destruction i.
+      + apply Hv.
+      + dependent destruction j.
+        * apply Hv.
+        * apply IH. intro k. apply Hv.
+  Qed.
+
+  Lemma cons_pool_sbisim {n} (t1 t2 : thread E) (v1 v2 : pool E n) :
+    t1 ~ t2 ->
+    pool_sbisim v1 v2 ->
+    pool_sbisim (cons_pool t1 v1) (cons_pool t2 v2).
+  Proof.
+    intros Ht Hv i.
+    refine (Fin.caseS' i (fun i => cons_pool t1 v1 i ~ cons_pool t2 v2 i) _ _).
+    - exact Ht.
+    - intro j. apply Hv.
+  Qed.
+
+  (** ** [equ]-level pool congruences, used by [schedule_pool_proper]. *)
+  Definition pool_equ {n : nat} (v1 v2 : pool E n) : Prop :=
+    forall i, v1 i ≅ v2 i.
+
+  Lemma replace_pool_equ {n} (v1 v2 : pool E n) (i : Fin.t n)
+        (t1 t2 : thread E) :
+    pool_equ v1 v2 ->
+    t1 ≅ t2 ->
+    pool_equ (replace_pool v1 i t1) (replace_pool v2 i t2).
+  Proof.
+    intros Hv Ht j.
+    unfold replace_pool.
+    destruct (Fin.eq_dec i j); auto.
+  Qed.
+
+  Lemma remove_pool_equ {n} (v1 v2 : pool E (S n)) (i : Fin.t (S n)) :
+    pool_equ v1 v2 ->
+    pool_equ (remove_pool v1 i) (remove_pool v2 i).
+  Proof.
+    intros Hv j.
+    revert v1 v2 i j Hv.
+    induction n as [| n IH]; intros v1 v2 i j Hv.
+    - dependent destruction j.
+    - cbn.
+      dependent destruction i.
+      + apply Hv.
+      + dependent destruction j.
+        * apply Hv.
+        * apply IH. intro k. apply Hv.
+  Qed.
+
+  Lemma cons_pool_equ {n} (t1 t2 : thread E) (v1 v2 : pool E n) :
+    t1 ≅ t2 ->
+    pool_equ v1 v2 ->
+    pool_equ (cons_pool t1 v1) (cons_pool t2 v2).
+  Proof.
+    intros Ht Hv i.
+    refine (Fin.caseS' i (fun i => cons_pool t1 v1 i ≅ cons_pool t2 v2 i) _ _).
+    - exact Ht.
+    - intro j. apply Hv.
+  Qed.
+End PoolSBisim.
+
+Section SchedulerTransitions.
+  Context {E : Type} `{Encode E}.
+
+  Lemma trans_schedule_no_focus_nonempty n (v : pool E (S n)) :
+    trans (obs (inl Yield : yieldE + (spawnE + E)) tt)
+      (schedule (S n) v None)
+      (Br n (fun i => schedule (S n) v (Some i))).
+  Proof.
+    unfold trans; cbn.
+    eapply (@Stepobs
+      (yieldE + (spawnE + E)) _ unit
+      (inl Yield) _ tt
+      (Br n (fun i => schedule (S n) v (Some i)))).
+    reflexivity.
+  Qed.
+
+  Lemma trans_schedule_no_focus_choose n (v : pool E (S n)) (i : Fin.t (S n)) :
+    trans tau
+      (Br n (fun i => schedule (S n) v (Some i)))
+      (schedule (S n) v (Some i)).
+  Proof.
+    apply trans_br with (x := i). reflexivity.
+  Qed.
+
+  Lemma trans_schedule_focused_yield n (v : pool E (S n)) (i : Fin.t (S n)) k :
+    observe (v i) = VisF (inl Yield) k ->
+    trans (obs (inl Yield : yieldE + (spawnE + E)) tt)
+      (schedule (S n) v (Some i))
+      (Br n (fun j => schedule (S n) (replace_pool v i (k tt)) (Some j))).
+  Proof.
+    intro Hobs.
+    unfold trans; lazy [schedule observe _observe].
+    change (@_observe _ _ unit (v i)) with (observe (v i)).
+    rewrite Hobs.
+    eapply Stepguard.
+    eapply (@Stepobs
+      (yieldE + (spawnE + E)) _ unit
+      (inl Yield) _ tt
+      (Br n (fun j => schedule (S n) (replace_pool v i (k tt)) (Some j)))).
+    reflexivity.
+  Qed.
+
+  Lemma trans_schedule_focused_fork n (v : pool E (S n)) (i : Fin.t (S n)) k :
+    observe (v i) = VisF (inr (inl Fork)) k ->
+    trans (obs (inr (inl Spawn) : yieldE + (spawnE + E)) tt)
+      (schedule (S n) v (Some i))
+      (schedule (S (S n))
+         (cons_pool (k true) (replace_pool v i (k false)))
+         (Some (Fin.FS i))).
+  Proof.
+    intro Hobs.
+    unfold trans; lazy [schedule observe _observe].
+    change (@_observe _ _ unit (v i)) with (observe (v i)).
+    rewrite Hobs.
+    eapply (@Stepobs
+      (yieldE + (spawnE + E)) _ unit
+      (inr (inl Spawn)) _ tt
+      (schedule (S (S n))
+         (cons_pool (k true) (replace_pool v i (k false)))
+         (Some (Fin.FS i)))).
+    reflexivity.
+  Qed.
+
+  Lemma trans_schedule_focused_user_event
+        n (v : pool E (S n)) (i : Fin.t (S n)) e k x :
+    observe (v i) = VisF (inr (inr e)) k ->
+    trans (obs (inr (inr e) : yieldE + (spawnE + E)) x)
+      (schedule (S n) v (Some i))
+      (schedule (S n) (replace_pool v i (k x)) (Some i)).
+  Proof.
+    intro Hobs.
+    unfold trans; lazy [schedule observe _observe].
+    change (@_observe _ _ unit (v i)) with (observe (v i)).
+    rewrite Hobs.
+    eapply (@Stepobs
+      (yieldE + (spawnE + E)) _ unit
+      (inr (inr e)) _ x
+      (schedule (S n) (replace_pool v i (k x)) (Some i))).
+    reflexivity.
+  Qed.
+
+  Lemma trans_schedule_focused_br
+        n (v : pool E (S n)) (i : Fin.t (S n)) b k (j : Fin.t (S b)) :
+    observe (v i) = BrF b k ->
+    trans tau (schedule (S n) v (Some i))
+      (schedule (S n) (replace_pool v i (k j)) (Some i)).
+  Proof.
+    intro Hobs.
+    unfold trans; lazy [schedule observe _observe].
+    change (@_observe _ _ unit (v i)) with (observe (v i)).
+    rewrite Hobs.
+    eapply (@Steptau
+      (yieldE + (spawnE + E)) _ unit b j _
+      (schedule (S n) (replace_pool v i (k j)) (Some i))).
+    reflexivity.
+  Qed.
+
+  (** ** Phase 2: remaining transition / unfold constructors. *)
+
+  Lemma trans_schedule_empty_ret (v : pool E 0) :
+    schedule 0 v None ≅ Ret tt.
+  Proof.
+    rewrite (ictree_eta (schedule 0 v None)).
+    rewrite schedule_empty_none.
+    reflexivity.
+  Qed.
+
+  Lemma trans_schedule_focused_ret n (v : pool E (S n)) (i : Fin.t (S n)) :
+    observe (v i) = RetF tt ->
+    schedule (S n) v (Some i) ≅ Guard (schedule n (remove_pool v i) None).
+  Proof.
+    intro Hobs.
+    rewrite (ictree_eta (schedule (S n) v (Some i))).
+    rewrite (schedule_focused_ret _ v i Hobs).
+    reflexivity.
+  Qed.
+
+  Lemma trans_schedule_focused_guard n (v : pool E (S n)) (i : Fin.t (S n)) t :
+    observe (v i) = GuardF t ->
+    schedule (S n) v (Some i)
+      ≅ Guard (schedule (S n) (replace_pool v i t) (Some i)).
+  Proof.
+    intro Hobs.
+    rewrite (ictree_eta (schedule (S n) v (Some i))).
+    rewrite (schedule_focused_guard _ v i t Hobs).
+    reflexivity.
+  Qed.
+
+  (** ** Phase 3: scheduler transition inversions. *)
+
+  Lemma schedule_no_focus_equ n (v : pool E (S n)) :
+    schedule (S n) v None
+      ≅ Vis (inl Yield : yieldE + (spawnE + E))
+          (fun _ => Br n (fun i => schedule (S n) v (Some i))).
+  Proof.
+    rewrite (ictree_eta (schedule (S n) v None)).
+    rewrite schedule_no_focus_nonempty.
+    reflexivity.
+  Qed.
+
+  Lemma trans_schedule_no_focus_inv n (v : pool E (S n)) l t' :
+    trans l (schedule (S n) v None) t' ->
+    l = obs (inl Yield : yieldE + (spawnE + E)) tt /\
+    t' ≅ Br n (fun i => schedule (S n) v (Some i)).
+  Proof.
+    intro TR.
+    rewrite schedule_no_focus_equ in TR.
+    apply trans_vis_inv in TR as (x & Heq & Hl).
+    destruct x.
+    split; auto.
+  Qed.
+
+  Lemma trans_schedule_focused_inv n (v : pool E (S n)) (i : Fin.t (S n)) l t' :
+    trans l (schedule (S n) v (Some i)) t' ->
+    (** focused [Ret]: collapse the [Guard], step the residual pool *)
+    (observe (v i) = RetF tt /\
+       trans l (schedule n (remove_pool v i) None) t')
+    \/
+    (** focused [Guard]: collapse, step the [replace_pool] residual *)
+    (exists g, observe (v i) = GuardF g /\
+       trans l (schedule (S n) (replace_pool v i g) (Some i)) t')
+    \/
+    (** focused [Br b k]: [tau] to one of the branches *)
+    (exists b k (j : Fin.t (S b)), observe (v i) = BrF b k /\
+       l = tau /\
+       t' ≅ schedule (S n) (replace_pool v i (k j)) (Some i))
+    \/
+    (** focused [Yield]: visible [Yield], [Br] back over the residual pool *)
+    (exists k, observe (v i) = VisF (inl Yield) k /\
+       l = obs (inl Yield : yieldE + (spawnE + E)) tt /\
+       t' ≅ Br n (fun j =>
+              schedule (S n) (replace_pool v i (k tt)) (Some j)))
+    \/
+    (** focused [Fork]: visible [Spawn], cons the child, focus it *)
+    (exists k, observe (v i) = VisF (inr (inl Fork)) k /\
+       l = obs (inr (inl Spawn) : yieldE + (spawnE + E)) tt /\
+       t' ≅ schedule (S (S n))
+              (cons_pool (k true) (replace_pool v i (k false)))
+              (Some (Fin.FS i)))
+    \/
+    (** focused user event [e]: visible [e], step the focused thread *)
+    (exists e k x, observe (v i) = VisF (inr (inr e)) k /\
+       l = obs (inr (inr e) : yieldE + (spawnE + E)) x /\
+       t' ≅ schedule (S n) (replace_pool v i (k x)) (Some i)).
+  Proof.
+    intro TR.
+    destruct (observe (v i)) as [r | b k | g | e k] eqn:Hobs.
+    - (* RetF *)
+      destruct r.
+      left.
+      split; auto.
+      rewrite (trans_schedule_focused_ret _ v i Hobs) in TR.
+      now apply trans_guard_inv in TR.
+    - (* BrF b k *)
+      do 2 right; left.
+      assert (Hsch := schedule_focused_br _ v i b k Hobs).
+      rewrite (ictree_eta (schedule (S n) v (Some i))) in TR.
+      rewrite Hsch in TR.
+      apply trans_br_inv in TR as (j & Heq & Hl).
+      exists b, k, j; auto.
+    - (* GuardF g *)
+      right; left.
+      exists g.
+      split; auto.
+      rewrite (trans_schedule_focused_guard _ v i g Hobs) in TR.
+      now apply trans_guard_inv in TR.
+    - (* VisF e k *)
+      destruct e as [yld | [frk | usr]].
+      + (* Yield *)
+        destruct yld.
+        do 3 right; left.
+        exists k.
+        split; auto.
+        rewrite (ictree_eta (schedule (S n) v (Some i))) in TR.
+        rewrite (schedule_focused_yield _ v i k Hobs) in TR.
+        apply trans_guard_inv in TR.
+        rewrite schedule_no_focus_equ in TR.
+        apply trans_vis_inv in TR as (x & Heq & Hl).
+        destruct x.
+        split; auto.
+      + (* Fork *)
+        destruct frk.
+        do 4 right; left.
+        exists k.
+        split; auto.
+        rewrite (ictree_eta (schedule (S n) v (Some i))) in TR.
+        rewrite (schedule_focused_fork _ v i k Hobs) in TR.
+        apply trans_vis_inv in TR as (x & Heq & Hl).
+        destruct x.
+        split; auto.
+      + (* user event *)
+        do 5 right.
+        rewrite (ictree_eta (schedule (S n) v (Some i))) in TR.
+        rewrite (schedule_focused_user_event _ v i usr k Hobs) in TR.
+        apply trans_vis_inv in TR as (x & Heq & Hl).
+        exists usr, k, x; auto.
+  Qed.
+
+  (** ** [schedule] respects [equ]-equality of pools, in every focus. *)
+  Lemma schedule_pool_proper n (v w : pool E n) focus :
+    pool_equ v w ->
+    schedule n v focus ≅ schedule n w focus.
+  Proof.
+    revert n v w focus.
+    coinduction R CH.
+    intros n v w focus Hvw.
+    destruct focus as [i |].
+    - destruct n as [| n']; [ inversion i |].
+      pose proof (Hvw i) as Hi.
+      assert (Hgo : go (observe (v i)) ≅ go (observe (w i))).
+      { rewrite <- !ictree_eta. exact Hi. }
+      rewrite (ictree_eta (schedule (S n') v (Some i))).
+      rewrite (ictree_eta (schedule (S n') w (Some i))).
+      destruct (observe (v i)) as [r | b k | g | e k] eqn:Hv;
+      destruct (observe (w i)) as [r2 | b2 k2 | g2 | e2 k2] eqn:Hw;
+        try (step in Hgo; inversion Hgo; fail).
+      + destruct r, r2.
+        rewrite (@schedule_focused_ret E _ n' v i Hv).
+        rewrite (@schedule_focused_ret E _ n' w i Hw).
+        cbn. constructor. apply CH. apply remove_pool_equ. exact Hvw.
+      + pose proof (equ_br_invT Hgo) as Hbeq; subst b2.
+        pose proof (equ_br_invE Hgo) as Hke.
+        rewrite (@schedule_focused_br E _ n' v i b k Hv).
+        rewrite (@schedule_focused_br E _ n' w i b k2 Hw).
+        cbn. constructor. intro j. apply CH.
+        apply replace_pool_equ. exact Hvw. apply Hke.
+      + pose proof (equ_guard_invE Hgo) as Hge.
+        rewrite (@schedule_focused_guard E _ n' v i g Hv).
+        rewrite (@schedule_focused_guard E _ n' w i g2 Hw).
+        cbn. constructor. apply CH.
+        apply replace_pool_equ. exact Hvw. exact Hge.
+      + pose proof (equ_vis_invT Hgo) as [_ Heeq]; subst e2.
+        pose proof (equ_vis_invE Hgo) as Hke.
+        destruct e as [yld | [frk | usr]].
+        * destruct yld.
+          rewrite (@schedule_focused_yield E _ n' v i k Hv).
+          rewrite (@schedule_focused_yield E _ n' w i k2 Hw).
+          cbn. constructor. apply CH.
+          apply replace_pool_equ. exact Hvw. apply (Hke tt).
+        * destruct frk.
+          rewrite (@schedule_focused_fork E _ n' v i k Hv).
+          rewrite (@schedule_focused_fork E _ n' w i k2 Hw).
+          cbn. constructor. intros _. apply CH.
+          apply cons_pool_equ.
+          -- apply (Hke true).
+          -- apply replace_pool_equ. exact Hvw. apply (Hke false).
+        * rewrite (@schedule_focused_user_event E _ n' v i usr k Hv).
+          rewrite (@schedule_focused_user_event E _ n' w i usr k2 Hw).
+          cbn. constructor. intro x. apply CH.
+          apply replace_pool_equ. exact Hvw. apply (Hke x).
+    - destruct n as [| n'].
+      + rewrite (ictree_eta (schedule 0 v None)).
+        rewrite (ictree_eta (schedule 0 w None)).
+        rewrite schedule_empty_none, schedule_empty_none.
+        cbn. reflexivity.
+      + rewrite (ictree_eta (schedule (S n') v None)).
+        rewrite (ictree_eta (schedule (S n') w None)).
+        rewrite schedule_no_focus_nonempty, schedule_no_focus_nonempty.
+        cbn. constructor. intros _. cbn. step.
+        constructor. intro i. apply CH. exact Hvw.
+  Qed.
+  (** ** Phase 4: thread-step to scheduler-step lifts. *)
+
+  Lemma pool_equ_refl {n} (v : pool E n) : pool_equ v v.
+  Proof. intro j; reflexivity. Qed.
+
+  Lemma replace_pool_idem_equ {n} (v : pool E (S n)) (i : Fin.t (S n))
+        (a b : thread E) :
+    pool_equ (replace_pool v i b) (replace_pool (replace_pool v i a) i b).
+  Proof. intro j. unfold replace_pool. destruct (Fin.eq_dec i j); reflexivity. Qed.
+
+  Lemma br_schedule_pool_equ {n} (v w : pool E (S n)) :
+    pool_equ v w ->
+    Br n (fun j => schedule (S n) v (Some j))
+      ≅ Br n (fun j => schedule (S n) w (Some j)).
+  Proof.
+    intro Hvw. step. constructor. intro j.
+    apply schedule_pool_proper. exact Hvw.
+  Qed.
+
+  Lemma schedule_lift_yield n (v : pool E (S n)) (i : Fin.t (S n))
+        (u : thread E) :
+    trans (obs (inl Yield : yieldE + (forkE + E)) tt) (v i) u ->
+    trans (obs (inl Yield : yieldE + (spawnE + E)) tt)
+      (schedule (S n) v (Some i))
+      (Br n (fun j => schedule (S n) (replace_pool v i u) (Some j))).
+  Proof.
+    intro TR.
+    unfold trans in TR.
+    remember (observe (v i)) as ot eqn:Hot.
+    remember (observe u) as ou eqn:Hou.
+    remember (obs (inl Yield : yieldE + (forkE + E)) tt) as lbl eqn:Hlbl.
+    revert v i u Hot Hou Hlbl.
+    induction TR; intros.
+    - (* Stepguard: observe (v i) = GuardF t *)
+      rewrite (trans_schedule_focused_guard n v i t (eq_sym Hot)).
+      apply trans_guard.
+      rewrite (br_schedule_pool_equ (replace_pool v i u0)
+                 (replace_pool (replace_pool v i t) i u0)
+                 (replace_pool_idem_equ v i t u0)).
+      apply (IHTR (replace_pool v i t) i u0).
+      + now rewrite replace_pool_hit.
+      + exact Hou.
+      + exact Hlbl.
+    - discriminate Hlbl.
+    - (* Stepobs *)
+      dependent destruction Hlbl.
+      assert (Hu0 : u ≅ k tt).
+      { transitivity t.
+        - rewrite (ictree_eta u), (ictree_eta t), <- Hou; reflexivity.
+        - symmetry; assumption. }
+      rewrite (br_schedule_pool_equ (replace_pool v i u)
+                 (replace_pool v i (k tt))
+                 (replace_pool_equ v v i u (k tt) (pool_equ_refl v) Hu0)).
+      apply (trans_schedule_focused_yield n v i k (eq_sym Hot)).
+    - discriminate Hlbl.
+  Qed.
+
+  Lemma schedule_some_pool_equ {m} (v w : pool E (S m)) (i : Fin.t (S m)) :
+    pool_equ v w ->
+    schedule (S m) v (Some i) ≅ schedule (S m) w (Some i).
+  Proof. intro Hvw. apply schedule_pool_proper. exact Hvw. Qed.
+
+  Lemma schedule_lift_user n (v : pool E (S n)) (i : Fin.t (S n))
+        (e : E) (x : encode e) (u : thread E) :
+    trans (obs (inr (inr e) : yieldE + (forkE + E)) x) (v i) u ->
+    trans (obs (inr (inr e) : yieldE + (spawnE + E)) x)
+      (schedule (S n) v (Some i))
+      (schedule (S n) (replace_pool v i u) (Some i)).
+  Proof.
+    intro TR.
+    unfold trans in TR.
+    remember (observe (v i)) as ot eqn:Hot.
+    remember (observe u) as ou eqn:Hou.
+    remember (obs (inr (inr e) : yieldE + (forkE + E)) x) as lbl eqn:Hlbl.
+    revert v i u Hot Hou Hlbl.
+    induction TR; intros.
+    - (* Stepguard *)
+      rewrite (trans_schedule_focused_guard n v i t (eq_sym Hot)).
+      apply trans_guard.
+      rewrite (schedule_some_pool_equ (replace_pool v i u0)
+                 (replace_pool (replace_pool v i t) i u0) i
+                 (replace_pool_idem_equ v i t u0)).
+      apply (IHTR (replace_pool v i t) i u0).
+      + now rewrite replace_pool_hit.
+      + exact Hou.
+      + exact Hlbl.
+    - discriminate Hlbl.
+    - (* Stepobs *)
+      dependent destruction Hlbl.
+      assert (Hu0 : u ≅ k x).
+      { transitivity t.
+        - rewrite (ictree_eta u), (ictree_eta t), <- Hou; reflexivity.
+        - symmetry; assumption. }
+      rewrite (schedule_some_pool_equ (replace_pool v i u)
+                 (replace_pool v i (k x)) i
+                 (replace_pool_equ v v i u (k x) (pool_equ_refl v) Hu0)).
+      apply (trans_schedule_focused_user_event n v i e k x (eq_sym Hot)).
+    - discriminate Hlbl.
+  Qed.
+
+  Lemma schedule_lift_tau n (v : pool E (S n)) (i : Fin.t (S n))
+        (u : thread E) :
+    trans tau (v i) u ->
+    trans tau
+      (schedule (S n) v (Some i))
+      (schedule (S n) (replace_pool v i u) (Some i)).
+  Proof.
+    intro TR.
+    unfold trans in TR.
+    remember (observe (v i)) as ot eqn:Hot.
+    remember (observe u) as ou eqn:Hou.
+    remember (tau : label (yieldE + (forkE + E))) as lbl eqn:Hlbl.
+    revert v i u Hot Hou Hlbl.
+    induction TR; intros.
+    - (* Stepguard *)
+      rewrite (trans_schedule_focused_guard n v i t (eq_sym Hot)).
+      apply trans_guard.
+      rewrite (schedule_some_pool_equ (replace_pool v i u0)
+                 (replace_pool (replace_pool v i t) i u0) i
+                 (replace_pool_idem_equ v i t u0)).
+      apply (IHTR (replace_pool v i t) i u0).
+      + now rewrite replace_pool_hit.
+      + exact Hou.
+      + exact Hlbl.
+    - (* Steptau *)
+      assert (Hu0 : u ≅ k x).
+      { transitivity t.
+        - rewrite (ictree_eta u), (ictree_eta t), <- Hou; reflexivity.
+        - symmetry; assumption. }
+      rewrite (schedule_some_pool_equ (replace_pool v i u)
+                 (replace_pool v i (k x)) i
+                 (replace_pool_equ v v i u (k x) (pool_equ_refl v) Hu0)).
+      apply (trans_schedule_focused_br n v i n0 k x (eq_sym Hot)).
+    - discriminate Hlbl.
+    - discriminate Hlbl.
+  Qed.
+
+  Lemma schedule_lift_fork n (v : pool E (S n)) (i : Fin.t (S n))
+        (b : bool) (u : thread E) :
+    trans (obs (inr (inl Fork) : yieldE + (forkE + E)) b) (v i) u ->
+    exists k2,
+      (forall c : bool,
+         trans (obs (inr (inl Fork) : yieldE + (forkE + E)) c) (v i) (k2 c)) /\
+      trans (obs (inr (inl Spawn) : yieldE + (spawnE + E)) tt)
+        (schedule (S n) v (Some i))
+        (schedule (S (S n))
+           (cons_pool (k2 true) (replace_pool v i (k2 false)))
+           (Some (Fin.FS i))).
+  Proof.
+    intro TR.
+    unfold trans in TR.
+    remember (observe (v i)) as ot eqn:Hot.
+    remember (observe u) as ou eqn:Hou.
+    remember (obs (inr (inl Fork) : yieldE + (forkE + E)) b) as lbl eqn:Hlbl.
+    revert v i u Hot Hou Hlbl.
+    induction TR; intros.
+    - (* Stepguard *)
+      destruct (IHTR (replace_pool v i t) i u0
+                  ltac:(now rewrite replace_pool_hit) Hou Hlbl)
+        as (k2 & Hcont & Hstep).
+      exists k2. split.
+      + intro c. specialize (Hcont c).
+        rewrite replace_pool_hit in Hcont.
+        rewrite (ictree_eta (v i)), <- Hot.
+        now apply trans_guard.
+      + rewrite (trans_schedule_focused_guard n v i t (eq_sym Hot)).
+        apply trans_guard.
+        rewrite (schedule_pool_proper (S (S n))
+                   (cons_pool (k2 true) (replace_pool v i (k2 false)))
+                   (cons_pool (k2 true)
+                      (replace_pool (replace_pool v i t) i (k2 false)))
+                   (Some (Fin.FS i))).
+        * exact Hstep.
+        * apply cons_pool_equ; [reflexivity |].
+          apply replace_pool_idem_equ.
+    - discriminate Hlbl.
+    - (* Stepobs *)
+      dependent destruction Hlbl.
+      exists k. split.
+      + intro c.
+        rewrite (ictree_eta (v i)), <- Hot.
+        apply trans_vis.
+      + apply (trans_schedule_focused_fork n v i k (eq_sym Hot)).
+    - discriminate Hlbl.
+  Qed.
+
+  Lemma cast_refl m (i : Fin.t m) : Fin.cast i eq_refl = i.
+  Proof. induction i; cbn; [reflexivity | now rewrite IHi]. Qed.
+
+  Lemma remove_pool_agree {n} :
+    forall (v w : pool E (S n)) (i : Fin.t (S n)),
+    (forall j, i <> j -> v j ≅ w j) ->
+    pool_equ (remove_pool v i) (remove_pool w i).
+  Proof.
+    induction n as [| n IH]; intros v w i Hag j.
+    - dependent destruction j.
+    - cbn. dependent destruction i.
+      + apply Hag. intro Hc; discriminate.
+      + dependent destruction j.
+        * apply Hag. intro Hc; discriminate.
+        * apply IH. intros k Hik.
+          rewrite (cast_refl _ i) in Hik.
+          apply Hag. intro Heq. apply Hik.
+          apply Fin.FS_inj. exact Heq.
+  Qed.
+
+  Lemma remove_replace_pool_equ {n} (v : pool E (S n)) (i : Fin.t (S n))
+        (a : thread E) :
+    pool_equ (remove_pool (replace_pool v i a) i) (remove_pool v i).
+  Proof.
+    apply remove_pool_agree. intros j Hij.
+    rewrite replace_pool_miss; [reflexivity | exact Hij].
+  Qed.
+
+  Lemma schedule_lift_ret n (v : pool E (S n)) (i : Fin.t (S n))
+        (u : thread E) :
+    trans (val tt : label (yieldE + (forkE + E))) (v i) u ->
+    schedule (S n) v (Some i) ~ schedule n (remove_pool v i) None.
+  Proof.
+    intro TR.
+    unfold trans in TR.
+    remember (observe (v i)) as ot eqn:Hot.
+    remember (observe u) as ou eqn:Hou.
+    remember (val tt : label (yieldE + (forkE + E))) as lbl eqn:Hlbl.
+    revert v i u Hot Hou Hlbl.
+    induction TR; intros.
+    - (* Stepguard *)
+      rewrite (trans_schedule_focused_guard n v i t (eq_sym Hot)).
+      rewrite sb_guard.
+      rewrite (IHTR (replace_pool v i t) i u0
+                 ltac:(now rewrite replace_pool_hit) Hou Hlbl).
+      now rewrite (schedule_pool_proper n (remove_pool (replace_pool v i t) i)
+               (remove_pool v i) None (remove_replace_pool_equ v i t)).
+    - discriminate Hlbl.
+    - discriminate Hlbl.
+    - (* Stepval *)
+      dependent destruction Hlbl.
+      rewrite (trans_schedule_focused_ret n v i (eq_sym Hot)).
+      apply sb_guard.
+  Qed.
+
+  (** ** Phase 5: [schedule] preserves pool strong bisimilarity. *)
+
+  Notation completed' := (completed E).
+  Notation stR R := (lattice.body (coinduction.t (sb eq)) R).
+
+  Lemma schedule_match (R : rel completed' completed')
+    (Hch : forall m (w1 w2 : pool E m) f,
+       pool_sbisim w1 w2 -> stR R (schedule m w1 f) (schedule m w2 f)) :
+    forall l os ot', trans_ l os ot' ->
+    forall n (v1 v2 : pool E n) focus (t' : completed'),
+      os = observe (schedule n v1 focus) ->
+      ot' = observe t' ->
+      pool_sbisim v1 v2 ->
+      exists u', trans l (schedule n v2 focus) u' /\ stR R t' u'.
+  Proof.
+    intros l os ot' TR.
+    induction TR; intros nn v1 v2 focus t' Hos Hot' Hpool.
+    - (* Stepguard *)
+      destruct focus as [i | ].
+      + destruct nn as [| n']; [inversion i | ].
+        destruct (observe (v1 i)) as [r0 | b0 k0 | g | e0 k0] eqn:Hvi.
+        * (* Ret: recurse on the smaller pool *)
+          destruct r0.
+          rewrite (schedule_focused_ret n' v1 i Hvi) in Hos.
+          dependent destruction Hos.
+          destruct (IHTR n' (remove_pool v1 i) (remove_pool v2 i) None t'
+                      eq_refl Hot' (remove_pool_sbisim v1 v2 i Hpool))
+            as (u' & Htru & Hresu).
+          assert (Hvr : v1 i ≅ Ret tt).
+          { rewrite (ictree_eta (v1 i)), Hvi. reflexivity. }
+          assert (Htrv : trans (val tt : label (yieldE + (forkE + E)))
+                           (v1 i) stuck).
+          { rewrite Hvr. apply trans_ret. }
+          destruct (sbisim_trans (v1 i) (v2 i) stuck (val tt) eq
+                      (Hpool i) Htrv) as (lv & uv & Htr2v & Hlv & Hsbv).
+          subst lv.
+          assert (Hlift : schedule (S n') v2 (Some i)
+                          ~ schedule n' (remove_pool v2 i) None).
+          { apply (schedule_lift_ret n' v2 i uv Htr2v). }
+          destruct (sbisim_trans (schedule n' (remove_pool v2 i) None)
+                      (schedule (S n') v2 (Some i)) u' l eq
+                      ltac:(symmetry; exact Hlift) Htru)
+            as (lq & uq & Htrq & Hlq & Hsbq).
+          subst lq.
+          exists uq. split.
+          -- exact Htrq.
+          -- rewrite <- Hsbq. exact Hresu.
+        * (* Br: schedule head is a Br, not a Guard *)
+          rewrite (schedule_focused_br n' v1 i b0 k0 Hvi) in Hos.
+          discriminate Hos.
+        * (* Guard: recurse on the same pool, focus unchanged *)
+          rewrite (schedule_focused_guard n' v1 i g Hvi) in Hos.
+          dependent destruction Hos.
+          apply (IHTR (S n') (replace_pool v1 i g) v2 (Some i) t'
+                   eq_refl Hot').
+          intro j. unfold replace_pool. destruct (Fin.eq_dec i j) as [Hij | Hij].
+          -- subst j.
+             assert (Hvg : v1 i ≅ Guard g).
+             { rewrite (ictree_eta (v1 i)), Hvi. reflexivity. }
+             transitivity (v1 i); [| apply Hpool].
+             rewrite Hvg. symmetry. apply sb_guard.
+          -- apply Hpool.
+        * (* Vis: Yield (Guard head), or Fork / user (Vis head) *)
+          destruct e0 as [yld | [frk | usr]].
+          -- (* Yield: invert the focused-yield residual directly *)
+             destruct yld.
+             rewrite (schedule_focused_yield n' v1 i k0 Hvi) in Hos.
+             dependent destruction Hos.
+             assert (TR0 : trans l
+               (schedule (S n') (replace_pool v1 i (k0 tt)) None) t').
+             { unfold trans. rewrite <- Hot'. exact TR. }
+             apply trans_schedule_no_focus_inv in TR0 as (Hl & Hbr).
+             subst l.
+             assert (Hvis : v1 i ≅ Vis (inl Yield) k0).
+             { rewrite (ictree_eta (v1 i)), Hvi. reflexivity. }
+             assert (Htry : trans
+               (obs (inl Yield : yieldE + (forkE + E)) tt) (v1 i) (k0 tt)).
+             { rewrite Hvis. apply trans_vis. }
+             destruct (sbisim_trans (v1 i) (v2 i) (k0 tt)
+                         (obs (inl Yield : yieldE + (forkE + E)) tt) eq
+                         (Hpool i) Htry) as (ly & uy & Htr2y & Hly & Hsby).
+             subst ly.
+             exists (Br n' (fun j =>
+               schedule (S n') (replace_pool v2 i uy) (Some j))). split.
+             ++ apply (schedule_lift_yield n' v2 i uy Htr2y).
+             ++ rewrite Hbr.
+                apply (coinduction.bt_t (sb eq)).
+                apply step_sb_br_id; [reflexivity | intro j].
+                apply Hch.
+                apply replace_pool_sbisim; assumption.
+          -- (* Fork: Vis head, not a Guard *)
+             destruct frk.
+             rewrite (schedule_focused_fork n' v1 i k0 Hvi) in Hos.
+             discriminate Hos.
+          -- (* user: Vis head, not a Guard *)
+             rewrite (schedule_focused_user_event n' v1 i usr k0 Hvi) in Hos.
+             discriminate Hos.
+      + destruct nn as [| n'].
+        * rewrite (schedule_empty_none v1) in Hos. discriminate Hos.
+        * rewrite (schedule_no_focus_nonempty n' v1) in Hos. discriminate Hos.
+    - (* Steptau *)
+      destruct focus as [i | ].
+      + destruct nn as [| n']; [inversion i | ].
+        destruct (observe (v1 i)) as [r0 | b0 k0 | g | e0 k0] eqn:Hvi.
+        * destruct r0. rewrite (schedule_focused_ret n' v1 i Hvi) in Hos.
+          discriminate Hos.
+        * rewrite (schedule_focused_br n' v1 i b0 k0 Hvi) in Hos.
+          dependent destruction Hos.
+          assert (Htr1 : trans tau (v1 i) (k0 x)).
+          { rewrite (ictree_eta (v1 i)), Hvi.
+            apply trans_br with (x := x). reflexivity. }
+          destruct (sbisim_trans (v1 i) (v2 i) (k0 x) tau eq (Hpool i) Htr1)
+            as (l' & u' & Htr2 & Hl' & Hsb).
+          subst l'.
+          exists (schedule (S n') (replace_pool v2 i u') (Some i)). split.
+          -- apply schedule_lift_tau. exact Htr2.
+          -- assert (Ht' : t' ≅ schedule (S n') (replace_pool v1 i (k0 x)) (Some i)).
+             { rewrite (ictree_eta t'), <- Hot', <- (ictree_eta t).
+               symmetry; assumption. }
+             rewrite Ht'. apply Hch.
+             apply replace_pool_sbisim; assumption.
+        * rewrite (schedule_focused_guard n' v1 i g Hvi) in Hos.
+          discriminate Hos.
+        * destruct e0 as [yld | [frk | usr]].
+          -- destruct yld.
+             rewrite (schedule_focused_yield n' v1 i k0 Hvi) in Hos.
+             discriminate Hos.
+          -- destruct frk.
+             rewrite (schedule_focused_fork n' v1 i k0 Hvi) in Hos.
+             discriminate Hos.
+          -- rewrite (schedule_focused_user_event n' v1 i usr k0 Hvi) in Hos.
+             discriminate Hos.
+      + destruct nn as [| n'].
+        * rewrite (schedule_empty_none v1) in Hos. discriminate Hos.
+        * rewrite (schedule_no_focus_nonempty n' v1) in Hos. discriminate Hos.
+    - (* Stepobs *)
+      destruct focus as [i | ].
+      + destruct nn as [| n']; [inversion i | ].
+        destruct (observe (v1 i)) as [r0 | b0 k0 | g | e1 k0] eqn:Hvi.
+        * destruct r0. rewrite (schedule_focused_ret n' v1 i Hvi) in Hos.
+          discriminate Hos.
+        * rewrite (schedule_focused_br n' v1 i b0 k0 Hvi) in Hos.
+          discriminate Hos.
+        * rewrite (schedule_focused_guard n' v1 i g Hvi) in Hos.
+          discriminate Hos.
+        * destruct e1 as [yld | [frk | usr]].
+          -- destruct yld.
+             rewrite (schedule_focused_yield n' v1 i k0 Hvi) in Hos.
+             discriminate Hos.
+          -- (* Fork *)
+             destruct frk.
+             rewrite (schedule_focused_fork n' v1 i k0 Hvi) in Hos.
+             dependent destruction Hos.
+             destruct x.
+             assert (Hvis : v1 i ≅ Vis (inr (inl Fork)) k0).
+             { rewrite (ictree_eta (v1 i)), Hvi. reflexivity. }
+             assert (Htrf : trans
+               (obs (inr (inl Fork) : yieldE + (forkE + E)) false) (v1 i)
+               (k0 false)).
+             { rewrite Hvis. apply trans_vis. }
+             destruct (sbisim_trans (v1 i) (v2 i) (k0 false)
+                         (obs (inr (inl Fork)) false) eq (Hpool i) Htrf)
+               as (lf & uf & Htr2 & Hlf & Hsbf).
+             subst lf.
+             destruct (schedule_lift_fork n' v2 i false uf Htr2)
+               as (kf & Hforall & Hstep).
+             exists (schedule (S (S n'))
+                       (cons_pool (kf true) (replace_pool v2 i (kf false)))
+                       (Some (Fin.FS i))).
+             split.
+             ++ exact Hstep.
+             ++ assert (Ht' : t' ≅ schedule (S (S n'))
+                  (cons_pool (k0 true) (replace_pool v1 i (k0 false)))
+                  (Some (Fin.FS i))).
+                { rewrite (ictree_eta t'), <- Hot', <- (ictree_eta t).
+                  symmetry; assumption. }
+                rewrite Ht'.
+                assert (Hii : v2 i ~ v1 i) by (symmetry; apply Hpool).
+                assert (Hkf : forall c, k0 c ~ kf c).
+                { intro c.
+                  destruct (sbisim_trans (v2 i) (v1 i) (kf c)
+                              (obs (inr (inl Fork)) c) eq Hii (Hforall c))
+                    as (lc & wc & Htrc & Hlc & Hsbc).
+                  subst lc.
+                  rewrite Hvis in Htrc.
+                  apply trans_vis_inv in Htrc as (y & Hwy & Hly).
+                  dependent destruction Hly.
+                  rewrite Hwy in Hsbc. symmetry; exact Hsbc. }
+                apply Hch.
+                apply cons_pool_sbisim.
+                ** apply Hkf.
+                ** apply replace_pool_sbisim; [exact Hpool | apply Hkf].
+          -- (* user event *)
+             rewrite (schedule_focused_user_event n' v1 i usr k0 Hvi) in Hos.
+             dependent destruction Hos.
+             assert (Hvis : v1 i ≅ Vis (inr (inr usr)) k0).
+             { rewrite (ictree_eta (v1 i)), Hvi. reflexivity. }
+             assert (Htru : trans
+               (obs (inr (inr usr) : yieldE + (forkE + E)) x) (v1 i) (k0 x)).
+             { rewrite Hvis. apply trans_vis. }
+             destruct (sbisim_trans (v1 i) (v2 i) (k0 x)
+                         (obs (inr (inr usr) : yieldE + (forkE + E)) x) eq
+                         (Hpool i) Htru)
+               as (lu & u' & Htr2 & Hlu & Hsbu).
+             subst lu.
+             exists (schedule (S n') (replace_pool v2 i u') (Some i)). split.
+             ++ apply (schedule_lift_user n' v2 i usr x u' Htr2).
+             ++ assert (Ht' : t' ≅
+                  schedule (S n') (replace_pool v1 i (k0 x)) (Some i)).
+                { rewrite (ictree_eta t'), <- Hot', <- (ictree_eta t).
+                  symmetry; assumption. }
+                rewrite Ht'. apply Hch.
+                apply replace_pool_sbisim; assumption.
+      + destruct nn as [| n'].
+        * rewrite (schedule_empty_none v1) in Hos. discriminate Hos.
+        * (* None nonempty Yield *)
+          rewrite (schedule_no_focus_nonempty n' v1) in Hos.
+          dependent destruction Hos.
+          destruct x.
+          exists (Br n' (fun j => schedule (S n') v2 (Some j))). split.
+          -- apply (trans_schedule_no_focus_nonempty n' v2).
+          -- assert (Ht' : t' ≅ Br n' (fun j => schedule (S n') v1 (Some j))).
+             { rewrite (ictree_eta t'), <- Hot', <- (ictree_eta t).
+               symmetry; assumption. }
+             rewrite Ht'.
+             apply (coinduction.bt_t (sb eq)).
+             apply step_sb_br_id; [reflexivity | intro j].
+             apply Hch. exact Hpool.
+    - (* Stepval *)
+      destruct focus as [i | ].
+      + destruct nn as [| n']; [inversion i | ].
+        destruct (observe (v1 i)) as [r0 | b k | g | e k] eqn:Hvi.
+        * destruct r0. rewrite (schedule_focused_ret n' v1 i Hvi) in Hos.
+          discriminate Hos.
+        * rewrite (schedule_focused_br n' v1 i b k Hvi) in Hos.
+          discriminate Hos.
+        * rewrite (schedule_focused_guard n' v1 i g Hvi) in Hos.
+          discriminate Hos.
+        * destruct e as [yld | [frk | usr]].
+          -- destruct yld.
+             rewrite (schedule_focused_yield n' v1 i k Hvi) in Hos.
+             discriminate Hos.
+          -- destruct frk.
+             rewrite (schedule_focused_fork n' v1 i k Hvi) in Hos.
+             discriminate Hos.
+          -- rewrite (schedule_focused_user_event n' v1 i usr k Hvi) in Hos.
+             discriminate Hos.
+      + destruct nn as [| n'].
+        * rewrite (schedule_empty_none v1) in Hos.
+          inversion Hos; subst.
+          exists stuck. split.
+          -- rewrite (trans_schedule_empty_ret v2). apply trans_ret.
+          -- assert (Ht' : t' ≅ stuck).
+             { rewrite (ictree_eta t'), <- Hot', <- (ictree_eta t).
+               symmetry; assumption. }
+             rewrite Ht'. reflexivity.
+        * rewrite (schedule_no_focus_nonempty n' v1) in Hos.
+          discriminate Hos.
+  Qed.
+
+  Theorem sbisim_schedule n (v1 v2 : pool E n) focus :
+    pool_sbisim v1 v2 -> schedule n v1 focus ~ schedule n v2 focus.
+  Proof.
+    revert n v1 v2 focus.
+    coinduction R CH.
+    intros n v1 v2 focus Hpool.
+    assert (Hch : forall m (w1 w2 : pool E m) f,
+       pool_sbisim w1 w2 -> stR R (schedule m w1 f) (schedule m w2 f)).
+    { intros m w1 w2 f Hw. apply CH. exact Hw. }
+    split.
+    - intros l t' TR.
+      destruct (schedule_match R Hch _ _ _ TR n v1 v2 focus t'
+                  eq_refl eq_refl Hpool) as (u' & Htru & Hres).
+      exists l, u'. split; [exact Htru | split; [exact Hres | reflexivity]].
+    - intros l t' TR.
+      destruct (schedule_match R Hch _ _ _ TR n v2 v1 focus t'
+                  eq_refl eq_refl (pool_sbisim_sym v1 v2 Hpool))
+        as (u' & Htru & Hres).
+      exists l, u'. split; [exact Htru | split].
+      + unfold Basics.flip. symmetry. exact Hres.
+      + reflexivity.
+  Qed.
+
+
+End SchedulerTransitions.
+
+(** ** Phase 6: scheduler-visible denotation respects thread bisimilarity. *)
+
+(** Two source statements with strongly-bisimilar thread denotations yield
+    strongly-bisimilar scheduler-visible computations.  This is the singleton
+    instance of [sbisim_schedule] for the start-up pool of [scheduled_visible]. *)
+Corollary sbisim_scheduled_visible (s1 s2 : YStmt) :
+  denote_stmt s1 ~ denote_stmt s2 ->
+  scheduled_visible s1 ~ scheduled_visible s2.
+Proof.
+  intro Hs.
+  unfold scheduled_visible.
+  apply sbisim_schedule.
+  intro i. exact Hs.
+Qed.
diff --git a/theories/Lang/Yield/Scheduler.v b/theories/Lang/Yield/Scheduler.v
new file mode 100644
index 0000000..e9e1782
--- /dev/null
+++ b/theories/Lang/Yield/Scheduler.v
@@ -0,0 +1,48 @@
+From Stdlib Require Import Fin.
+From TICL Require Import ICTree.Core Events.Core Lang.Yield.Events Lang.Yield.Vec.
+
+Import ICtree ICTreeNotations.
+Local Open Scope ictree_scope.
+
+Section Scheduler.
+  Context {E : Type} `{Encode E}.
+
+  (** Cooperative scheduler for a finite pool.
+
+      [None] focus means the scheduler chooses a runnable thread after emitting
+      a scheduling [Yield].  [Some i] observes one step of thread [i], removing
+      finished threads, clearing focus on source yields, and turning source forks
+      into scheduler-visible [Spawn] events. *)
+  CoFixpoint schedule (n : nat) (v : pool E n) (focus : option (Fin.t n)) : completed E :=
+    match focus with
+    | None =>
+        match n return pool E n -> completed E with
+        | 0 => fun _ => Ret tt
+        | S n' => fun v => Vis (inl Yield) (fun _ => Br n' (fun i => schedule (S n') v (Some i)))
+        end v
+    | Some i =>
+        match n return pool E n -> Fin.t n -> completed E with
+        | 0 => fun _ i => match i with end
+        | S n' => fun v i =>
+            match observe (v i) with
+            | RetF _ => Guard (schedule n' (remove_pool v i) None)
+            | BrF b k => Br b (fun j => schedule (S n') (replace_pool v i (k j)) (Some i))
+            | GuardF t => Guard (schedule (S n') (replace_pool v i t) (Some i))
+            | VisF e k =>
+                match e as e0 return (encode e0 -> thread E) -> completed E with
+                | inl Yield => fun k => Guard (schedule (S n') (replace_pool v i (k tt)) None)
+                | inr (inl Fork) => fun k =>
+                    @go (yieldE + (spawnE + E)) _ unit
+                      (VisF ((inr (inl Spawn)) : yieldE + (spawnE + E))
+                         (fun _ => schedule (S (S n'))
+                                     (cons_pool (k true) (replace_pool v i (k false)))
+                                     (Some (FS i))))
+                | inr (inr e') => fun k =>
+                    @go (yieldE + (spawnE + E)) _ unit
+                      (VisF ((inr (inr e')) : yieldE + (spawnE + E))
+                         (fun x => schedule (S n') (replace_pool v i (k x)) (Some i)))
+                end k
+            end
+        end v i
+    end.
+End Scheduler.
diff --git a/theories/Lang/Yield/SchedulerFairness.v b/theories/Lang/Yield/SchedulerFairness.v
new file mode 100644
index 0000000..e7bd815
--- /dev/null
+++ b/theories/Lang/Yield/SchedulerFairness.v
@@ -0,0 +1,2519 @@
+From Stdlib Require Import
+  Fin
+  Program.Equality.
+From Coinduction Require Import lattice.
+From TICL Require Import
+  ICTree.Core
+  ICTree.Equ
+  ICTree.Interp.Core
+  ICTree.Logic.AF
+  ICTree.Logic.AG
+  ICTree.Logic.CanStep
+  ICTree.Logic.Trans
+  ICTree.Trans
+  Events.Core
+  Logic.Core
+  Logic.Kripke
+  Lang.Yield.Events
+  Lang.Yield.Scheduler
+  Lang.Yield.SBisim
+  Lang.Yield.Ticl
+  Lang.Yield.Vec
+  ICTree.SBisim.
+
+Import ICtree ICTreeNotations TiclNotations.
+Local Open Scope ictree_scope.
+Local Open Scope ticl_scope.
+
+(** Proof-facing scheduler observations for local fairness reasoning.
+
+    The core scheduler is left unchanged.  This module mirrors [schedule] with
+    an additive observation tier that records no-focus scheduling points and
+    the finite set of slots offered at each such point. *)
+
+Definition LiveSlot (n : nat) : Type := Fin.t n.
+
+Record SlotRef : Type := {
+  slot_pool_size : nat;
+  slot_live_slot : LiveSlot slot_pool_size;
+}.
+
+Definition live_slot_ref {n : nat} (i : LiveSlot n) : SlotRef :=
+  {| slot_pool_size := n; slot_live_slot := i |}.
+
+Variant SchedulerObs : Type :=
+| ObsSchedulingPoint : nat -> SchedulerObs
+| ObsOffered : SlotRef -> SchedulerObs.
+
+Definition schedulerObsE : Type := SchedulerObs.
+
+#[global] Instance Encode_schedulerObsE : Encode SchedulerObs :=
+  fun _ => unit.
+
+Definition scheduler_observedE (E : Type) : Type :=
+  schedulerObsE + (yieldE + (spawnE + E)).
+
+Definition observed_completed (E : Type) `{Encode E} : Type :=
+  ictree (scheduler_observedE E) unit.
+
+Definition observed_scheduling_point (n : nat) (obs : schedulerObsE) : Prop :=
+  obs = ObsSchedulingPoint n.
+
+Definition offer_live_slot_obs (n : nat) (i : LiveSlot n)
+    (obs : schedulerObsE) : Prop :=
+  obs = ObsOffered (live_slot_ref i).
+
+Definition offer_live_slot {E : Type} `{Encode E}
+    (n : nat) (i : LiveSlot n) : ticll (scheduler_observedE E) :=
+  CNow (fun w => w = Obs (inl (ObsOffered (live_slot_ref i))) tt).
+
+Definition recognize_live_slot {E : Type} `{Encode E}
+    (n : nat) (_ : pool E n) (_ : LiveSlot n) : Prop :=
+  True.
+
+Lemma fin_cast_refl {n : nat} (i : Fin.t n) :
+  Fin.cast i eq_refl = i.
+Proof. induction i; cbn; congruence. Qed.
+
+Lemma live_slot_one_eq (i j : LiveSlot 1) : i = j.
+Proof.
+  refine (Fin.caseS' i (fun i => forall j, i = j) _ _ j).
+  - intro j'.
+    refine (Fin.caseS' j' (fun j => Fin.F1 = j) eq_refl _).
+    intro j0.
+    exact (Fin.case0 (fun j0 => Fin.F1 = Fin.FS j0) j0).
+  - intro i0.
+    exact (Fin.case0 (fun i0 => forall j, Fin.FS i0 = j) i0).
+Qed.
+
+Section ObservedScheduler.
+  Context {E : Type} `{Encode E}.
+
+  Definition emit_scheduler_obs (obs : schedulerObsE) : observed_completed E :=
+    Vis (inl obs) (fun _ : unit => Ret tt).
+
+  Fixpoint emit_live_slot_offers_into_then
+      (m n : nat) (embed : LiveSlot n -> LiveSlot m)
+      (k : observed_completed E) {struct n} : observed_completed E :=
+    match n return (LiveSlot n -> LiveSlot m) -> observed_completed E with
+    | 0 => fun _ => k
+    | S n' => fun embed =>
+        Vis (inl (ObsOffered (live_slot_ref (embed Fin.F1))))
+          (fun _ : unit =>
+             emit_live_slot_offers_into_then m n'
+               (fun i => embed (Fin.FS i)) k)
+    end embed.
+
+  Definition emit_live_slot_offers_then
+      (n : nat) (k : observed_completed E) : observed_completed E :=
+    emit_live_slot_offers_into_then n n (fun i => i) k.
+
+  Definition emit_live_slot_offers (n : nat) : observed_completed E :=
+    emit_live_slot_offers_then n (Ret tt).
+
+  (** Observed scheduler.  The only extra visible events are proof-facing
+      [schedulerObsE] events at nonempty no-focus scheduling points. *)
+  CoFixpoint schedule_with_offers
+      (n : nat) (v : pool E n) (focus : option (Fin.t n))
+      : observed_completed E :=
+    match focus with
+    | None =>
+        match n return pool E n -> observed_completed E with
+        | 0 => fun _ => Ret tt
+        | S n' => fun v =>
+            Vis (inl (ObsSchedulingPoint (S n')))
+              (fun _ : unit =>
+                 schedule_with_offers_offer_prefix (S n') (S n')
+                   (fun i => i) v)
+        end v
+    | Some i =>
+        match n return pool E n -> Fin.t n -> observed_completed E with
+        | 0 => fun _ i => match i with end
+        | S n' => fun v i =>
+            match observe (v i) with
+            | RetF _ =>
+                Guard (schedule_with_offers n' (remove_pool v i) None)
+            | BrF b k =>
+                Br b (fun j =>
+                  schedule_with_offers (S n')
+                    (replace_pool v i (k j)) (Some i))
+            | GuardF t =>
+                Guard (schedule_with_offers (S n')
+                  (replace_pool v i t) (Some i))
+            | VisF e k =>
+                match e as e0 return
+                    (encode e0 -> thread E) -> observed_completed E with
+                | inl Yield => fun k =>
+                    Guard (schedule_with_offers (S n')
+                      (replace_pool v i (k tt)) None)
+                | inr (inl Fork) => fun k =>
+                    @go (scheduler_observedE E) _ unit
+                      (VisF (inr (inr (inl Spawn))
+                         : scheduler_observedE E)
+                        (fun _ => schedule_with_offers (S (S n'))
+                          (cons_pool (k true)
+                            (replace_pool v i (k false)))
+                          (Some (Fin.FS i))))
+                | inr (inr e') => fun k =>
+                    @go (scheduler_observedE E) _ unit
+                      (VisF (inr (inr (inr e'))
+                         : scheduler_observedE E)
+                        (fun x => schedule_with_offers (S n')
+                          (replace_pool v i (k x)) (Some i)))
+                end k
+            end
+        end v i
+    end
+  with schedule_with_offers_offer_prefix
+      (pool_size remaining : nat)
+      (embed : LiveSlot remaining -> LiveSlot pool_size)
+      (v : pool E pool_size) : observed_completed E :=
+    match remaining return
+        (LiveSlot remaining -> LiveSlot pool_size) ->
+        pool E pool_size -> observed_completed E with
+    | 0 => fun _ v =>
+        match pool_size return pool E pool_size -> observed_completed E with
+        | 0 => fun _ => Ret tt
+        | S n' => fun v =>
+            Vis (inr (inl Yield) : scheduler_observedE E)
+              (fun _ : unit =>
+                 Br n' (fun i =>
+                   schedule_with_offers (S n') v (Some i)))
+        end v
+    | S n' => fun embed v =>
+        Vis (inl (ObsOffered (live_slot_ref (embed Fin.F1))))
+          (fun _ : unit =>
+             schedule_with_offers_offer_prefix pool_size n'
+               (fun i => embed (Fin.FS i)) v)
+    end embed v.
+
+  Definition observe_scheduler_offers
+      (n : nat) (v : pool E n) (focus : option (Fin.t n))
+      : observed_completed E :=
+    schedule_with_offers n v focus.
+
+  Definition handle_scheduler_offers
+      : scheduler_observedE E ~> ictree (yieldE + (spawnE + E)) :=
+    fun event =>
+      match event with
+      | inl _ => Ret tt
+      | inr event' => ICtree.trigger event'
+      end.
+
+  Definition forget_scheduler_offers {X}
+      (t : ictree (scheduler_observedE E) X)
+      : ictree (yieldE + (spawnE + E)) X :=
+    interp handle_scheduler_offers t.
+
+  Lemma handle_scheduler_offers_obs obs :
+    handle_scheduler_offers (inl obs) = Ret tt.
+  Proof. reflexivity. Qed.
+
+  Lemma handle_scheduler_offers_visible event :
+    handle_scheduler_offers (inr event) = ICtree.trigger event.
+  Proof. reflexivity. Qed.
+
+  Lemma forget_scheduler_offers_no_focus_nonempty_unfold n
+      (v : pool E (S n)) :
+    forget_scheduler_offers (schedule_with_offers (S n) v None) ≅
+      Guard (forget_scheduler_offers
+        (schedule_with_offers_offer_prefix (S n) (S n)
+          (fun i : LiveSlot (S n) => i) v)).
+  Proof.
+    unfold forget_scheduler_offers.
+    rewrite unfold_interp.
+    cbn. rewrite bind_ret_l. reflexivity.
+  Qed.
+
+  Theorem forget_scheduler_offers_preserves_schedule_exact_no_focus_impossible n
+      (v : pool E (S n)) :
+    ~ forget_scheduler_offers (schedule_with_offers (S n) v None) ≅
+        schedule (S n) v None.
+  Proof.
+    intro Heq.
+    step in Heq.
+    cbn in Heq.
+    inversion Heq.
+  Qed.
+
+  Lemma forget_scheduler_offers_offer_prefix_succ_stutter m n
+      (embed : LiveSlot (S n) -> LiveSlot m) (v : pool E m) :
+    forget_scheduler_offers
+      (schedule_with_offers_offer_prefix m (S n) embed v) ~
+    forget_scheduler_offers
+      (schedule_with_offers_offer_prefix m n
+        (fun i => embed (Fin.FS i)) v).
+  Proof.
+    unfold forget_scheduler_offers.
+    rewrite unfold_interp.
+    cbn. rewrite bind_ret_l.
+    apply sb_guard.
+  Qed.
+
+  Lemma forget_scheduler_offers_offer_prefix_stutter m r
+      (embed : LiveSlot r -> LiveSlot m) (v : pool E m) :
+    forget_scheduler_offers
+      (schedule_with_offers_offer_prefix m r embed v) ~
+    forget_scheduler_offers
+      (schedule_with_offers_offer_prefix m 0
+        (fun i : LiveSlot 0 => match i with end) v).
+  Proof.
+    revert m embed v.
+    induction r as [| r IHr]; intros m embed v.
+    - destruct m as [| m'].
+      + unfold forget_scheduler_offers.
+        rewrite !unfold_interp.
+        cbn.
+        apply sb_ret. reflexivity.
+      + unfold forget_scheduler_offers.
+        rewrite !unfold_interp.
+        cbn.
+        reflexivity.
+    - transitivity (forget_scheduler_offers
+        (schedule_with_offers_offer_prefix m r
+          (fun i => embed (Fin.FS i)) v)).
+      + apply forget_scheduler_offers_offer_prefix_succ_stutter.
+      + apply IHr.
+  Qed.
+
+  Lemma forget_scheduler_offers_no_focus_stutters_to_offer_prefix n
+      (v : pool E (S n)) :
+    forget_scheduler_offers (schedule_with_offers (S n) v None) ~
+    forget_scheduler_offers
+      (schedule_with_offers_offer_prefix (S n) (S n)
+        (fun i : LiveSlot (S n) => i) v).
+  Proof.
+    rewrite forget_scheduler_offers_no_focus_nonempty_unfold.
+    apply sb_guard.
+  Qed.
+
+  Lemma forget_scheduler_offers_offer_prefix_zero_nonempty_unfold n
+      (embed : LiveSlot 0 -> LiveSlot (S n)) (v : pool E (S n)) :
+    forget_scheduler_offers
+      (schedule_with_offers_offer_prefix (S n) 0 embed v) ~
+    Vis (inl Yield)
+      (fun _ : unit =>
+         Br n (fun i =>
+           forget_scheduler_offers
+             (schedule_with_offers (S n) v (Some i)))).
+  Proof.
+    unfold forget_scheduler_offers.
+    rewrite unfold_interp.
+    cbn.
+    unfold ICtree.trigger, resum, ReSum_refl, resum_ret,
+      ReSumRet_refl.
+    rewrite bind_vis.
+    setoid_rewrite bind_ret_l.
+    apply sb_vis. intros [].
+    apply sb_guard_l.
+    unfold forget_scheduler_offers.
+    rewrite unfold_interp.
+    cbn.
+    apply sb_br_id. intro i.
+    apply sb_guard.
+  Qed.
+
+  Lemma forget_scheduler_offers_no_focus_projection_to_focused n
+      (v : pool E (S n)) :
+    forget_scheduler_offers (schedule_with_offers (S n) v None) ~
+    Vis (inl Yield)
+      (fun _ : unit =>
+         Br n (fun i =>
+           forget_scheduler_offers
+             (schedule_with_offers (S n) v (Some i)))).
+  Proof.
+    transitivity (forget_scheduler_offers
+      (schedule_with_offers_offer_prefix (S n) (S n)
+        (fun i : LiveSlot (S n) => i) v)).
+    - apply forget_scheduler_offers_no_focus_stutters_to_offer_prefix.
+    - transitivity (forget_scheduler_offers
+        (schedule_with_offers_offer_prefix (S n) 0
+          (fun i : LiveSlot 0 => match i with end) v)).
+      + apply forget_scheduler_offers_offer_prefix_stutter.
+      + apply forget_scheduler_offers_offer_prefix_zero_nonempty_unfold.
+  Qed.
+
+  Lemma emit_live_slot_offers_into_then_zero m
+      (embed : LiveSlot 0 -> LiveSlot m) k :
+    emit_live_slot_offers_into_then m 0 embed k = k.
+  Proof. reflexivity. Qed.
+
+  Lemma emit_live_slot_offers_into_then_succ m n
+      (embed : LiveSlot (S n) -> LiveSlot m) k :
+    observe (emit_live_slot_offers_into_then m (S n) embed k) =
+      VisF (inl (ObsOffered (live_slot_ref (embed Fin.F1))))
+        (fun _ : unit =>
+           emit_live_slot_offers_into_then m n
+             (fun i => embed (Fin.FS i)) k).
+  Proof. reflexivity. Qed.
+
+  Lemma emit_live_slot_offers_zero :
+    observe (emit_live_slot_offers 0) = RetF tt.
+  Proof. reflexivity. Qed.
+
+  Lemma emit_live_slot_offers_succ n :
+    observe (emit_live_slot_offers (S n)) =
+      VisF (inl (ObsOffered (live_slot_ref (Fin.F1 : LiveSlot (S n)))))
+        (fun _ : unit =>
+           emit_live_slot_offers_into_then (S n) n
+             (fun i => Fin.FS i) (Ret tt)).
+  Proof. reflexivity. Qed.
+
+  Local Ltac solve_focused_schedule_with_offers H :=
+    lazy [schedule_with_offers observe _observe];
+    match type of H with
+    | observe (?v ?i) = _ =>
+        change (@_observe _ _ unit (v i)) with (observe (v i));
+        rewrite H;
+        reflexivity
+    end.
+
+  Lemma schedule_with_offers_empty_none (v : pool E 0) :
+    observe (schedule_with_offers 0 v None) = RetF tt.
+  Proof. reflexivity. Qed.
+
+  Lemma schedule_with_offers_no_focus_nonempty n
+      (v : pool E (S n)) :
+    observe (schedule_with_offers (S n) v None) =
+      VisF (inl (ObsSchedulingPoint (S n)))
+        (fun _ : unit =>
+           schedule_with_offers_offer_prefix (S n) (S n)
+             (fun i => i) v).
+  Proof. reflexivity. Qed.
+
+  Lemma schedule_with_offers_offer_prefix_zero m
+      (embed : LiveSlot 0 -> LiveSlot m) (v : pool E m) :
+    observe (schedule_with_offers_offer_prefix m 0 embed v) =
+      match m return pool E m -> ictree' (scheduler_observedE E) unit with
+      | 0 => fun _ => RetF tt
+      | S n => fun v =>
+          VisF (inr (inl Yield) : scheduler_observedE E)
+            (fun _ : unit =>
+               Br n (fun i => schedule_with_offers (S n) v (Some i)))
+      end v.
+  Proof. destruct m; reflexivity. Qed.
+
+  Lemma schedule_with_offers_offer_prefix_succ m n
+      (embed : LiveSlot (S n) -> LiveSlot m) (v : pool E m) :
+    observe (schedule_with_offers_offer_prefix m (S n) embed v) =
+      VisF (inl (ObsOffered (live_slot_ref (embed Fin.F1))))
+        (fun _ : unit =>
+           schedule_with_offers_offer_prefix m n
+             (fun i => embed (Fin.FS i)) v).
+  Proof. reflexivity. Qed.
+
+  Lemma schedule_with_offers_focused_ret n
+      (v : pool E (S n)) (i : Fin.t (S n)) :
+    observe (v i) = RetF tt ->
+    observe (schedule_with_offers (S n) v (Some i)) =
+      GuardF (schedule_with_offers n (remove_pool v i) None).
+  Proof.
+    intro Hret.
+    solve_focused_schedule_with_offers Hret.
+  Qed.
+
+  Lemma schedule_with_offers_focused_br n
+      (v : pool E (S n)) (i : Fin.t (S n)) b k :
+    observe (v i) = BrF b k ->
+    observe (schedule_with_offers (S n) v (Some i)) =
+      BrF b (fun j =>
+        schedule_with_offers (S n) (replace_pool v i (k j)) (Some i)).
+  Proof.
+    intro Hbr.
+    solve_focused_schedule_with_offers Hbr.
+  Qed.
+
+  Lemma schedule_with_offers_focused_guard n
+      (v : pool E (S n)) (i : Fin.t (S n)) t :
+    observe (v i) = GuardF t ->
+    observe (schedule_with_offers (S n) v (Some i)) =
+      GuardF (schedule_with_offers (S n) (replace_pool v i t) (Some i)).
+  Proof.
+    intro Hg.
+    solve_focused_schedule_with_offers Hg.
+  Qed.
+
+  Lemma schedule_with_offers_focused_yield n
+      (v : pool E (S n)) (i : Fin.t (S n)) k :
+    observe (v i) = VisF (inl Yield) k ->
+    observe (schedule_with_offers (S n) v (Some i)) =
+      GuardF (schedule_with_offers (S n)
+        (replace_pool v i (k tt)) None).
+  Proof.
+    intro Hy.
+    solve_focused_schedule_with_offers Hy.
+  Qed.
+
+  Lemma schedule_with_offers_focused_fork n
+      (v : pool E (S n)) (i : Fin.t (S n)) k :
+    observe (v i) = VisF (inr (inl Fork)) k ->
+    observe (schedule_with_offers (S n) v (Some i)) =
+      VisF (inr (inr (inl Spawn)) : scheduler_observedE E)
+        (fun _ => schedule_with_offers (S (S n))
+          (cons_pool (k true) (replace_pool v i (k false)))
+          (Some (Fin.FS i))).
+  Proof.
+    intro Hf.
+    solve_focused_schedule_with_offers Hf.
+  Qed.
+
+  Lemma schedule_with_offers_focused_user_event n
+      (v : pool E (S n)) (i : Fin.t (S n)) e k :
+    observe (v i) = VisF (inr (inr e)) k ->
+    observe (schedule_with_offers (S n) v (Some i)) =
+      VisF (inr (inr (inr e)) : scheduler_observedE E)
+        (fun x => schedule_with_offers (S n)
+          (replace_pool v i (k x)) (Some i)).
+  Proof.
+    intro Hu.
+    solve_focused_schedule_with_offers Hu.
+  Qed.
+
+  Lemma focused_yield_returns_to_scheduling_point n
+      (v : pool E (S n)) (i : Fin.t (S n)) k :
+    observe (v i) = VisF (inl Yield) k ->
+    observe (schedule_with_offers (S n) v (Some i)) =
+      GuardF (schedule_with_offers (S n)
+        (replace_pool v i (k tt)) None).
+  Proof. apply schedule_with_offers_focused_yield. Qed.
+
+  Lemma forget_scheduler_offers_empty_no_focus_projection
+      (v : pool E 0) :
+    forget_scheduler_offers (schedule_with_offers 0 v None) ~ Ret tt.
+  Proof.
+    unfold forget_scheduler_offers.
+    rewrite unfold_interp.
+    cbn.
+    apply sb_ret. reflexivity.
+  Qed.
+
+  Lemma forget_scheduler_offers_focused_ret_projection n
+      (v : pool E (S n)) (i : Fin.t (S n)) :
+    observe (v i) = RetF tt ->
+    forget_scheduler_offers (schedule_with_offers (S n) v (Some i)) ~
+    forget_scheduler_offers (schedule_with_offers n (remove_pool v i) None).
+  Proof.
+    intro Hret.
+    unfold forget_scheduler_offers.
+    rewrite unfold_interp.
+    rewrite (schedule_with_offers_focused_ret n v i Hret).
+    cbn.
+    apply sb_guard.
+  Qed.
+
+  Lemma forget_scheduler_offers_focused_br_projection n
+      (v : pool E (S n)) (i : Fin.t (S n)) b k :
+    observe (v i) = BrF b k ->
+    forget_scheduler_offers (schedule_with_offers (S n) v (Some i)) ~
+    Br b (fun j =>
+      forget_scheduler_offers
+        (schedule_with_offers (S n) (replace_pool v i (k j)) (Some i))).
+  Proof.
+    intro Hbr.
+    unfold forget_scheduler_offers.
+    rewrite unfold_interp.
+    rewrite (schedule_with_offers_focused_br n v i b k Hbr).
+    cbn.
+    apply sb_br_id. intro j.
+    apply sb_guard.
+  Qed.
+
+  Lemma forget_scheduler_offers_focused_guard_projection n
+      (v : pool E (S n)) (i : Fin.t (S n)) t :
+    observe (v i) = GuardF t ->
+    forget_scheduler_offers (schedule_with_offers (S n) v (Some i)) ~
+    forget_scheduler_offers
+      (schedule_with_offers (S n) (replace_pool v i t) (Some i)).
+  Proof.
+    intro Hguard.
+    unfold forget_scheduler_offers.
+    rewrite unfold_interp.
+    rewrite (schedule_with_offers_focused_guard n v i t Hguard).
+    cbn.
+    apply sb_guard.
+  Qed.
+
+  Lemma forget_scheduler_offers_focused_yield_projection n
+      (v : pool E (S n)) (i : Fin.t (S n)) k :
+    observe (v i) = VisF (inl Yield) k ->
+    forget_scheduler_offers (schedule_with_offers (S n) v (Some i)) ~
+    forget_scheduler_offers
+      (schedule_with_offers (S n) (replace_pool v i (k tt)) None).
+  Proof.
+    intro Hyield.
+    unfold forget_scheduler_offers.
+    rewrite unfold_interp.
+    rewrite (schedule_with_offers_focused_yield n v i k Hyield).
+    cbn.
+    apply sb_guard.
+  Qed.
+
+  Lemma forget_scheduler_offers_focused_fork_projection n
+      (v : pool E (S n)) (i : Fin.t (S n)) k :
+    observe (v i) = VisF (inr (inl Fork)) k ->
+    forget_scheduler_offers (schedule_with_offers (S n) v (Some i)) ~
+    Vis (inr (inl Spawn) : yieldE + (spawnE + E))
+      (fun _ =>
+        forget_scheduler_offers (schedule_with_offers (S (S n))
+          (cons_pool (k true) (replace_pool v i (k false)))
+          (Some (Fin.FS i)))).
+  Proof.
+    intro Hfork.
+    unfold forget_scheduler_offers.
+    rewrite unfold_interp.
+    rewrite (schedule_with_offers_focused_fork n v i k Hfork).
+    cbn.
+    unfold ICtree.trigger, resum, ReSum_refl, resum_ret,
+      ReSumRet_refl.
+    rewrite bind_vis.
+    setoid_rewrite bind_ret_l.
+    apply sb_vis. intros [].
+    apply sb_guard.
+  Qed.
+
+  Lemma forget_scheduler_offers_focused_user_event_projection n
+      (v : pool E (S n)) (i : Fin.t (S n)) e k :
+    observe (v i) = VisF (inr (inr e)) k ->
+    forget_scheduler_offers (schedule_with_offers (S n) v (Some i)) ~
+    Vis (inr (inr e) : yieldE + (spawnE + E))
+      (fun x =>
+        forget_scheduler_offers
+          (schedule_with_offers (S n) (replace_pool v i (k x)) (Some i))).
+  Proof.
+    intro Huser.
+    unfold forget_scheduler_offers.
+    rewrite unfold_interp.
+    rewrite (schedule_with_offers_focused_user_event n v i e k Huser).
+    cbn.
+    unfold ICtree.trigger, resum, ReSum_refl, resum_ret,
+      ReSumRet_refl.
+    rewrite bind_vis.
+    setoid_rewrite bind_ret_l.
+    apply sb_vis. intro x.
+    apply sb_guard.
+  Qed.
+
+  Local Notation completed' := (completed E).
+  Local Notation stR R := (lattice.body (coinduction.t (sb eq)) R).
+
+  Local Definition erased_schedule (n : nat) (v : pool E n)
+      (focus : option (Fin.t n)) : completed E :=
+    forget_scheduler_offers (schedule_with_offers n v focus).
+
+  Local Lemma erased_focused_ret_equ n
+      (v : pool E (S n)) (i : Fin.t (S n)) :
+    observe (v i) = RetF tt ->
+    erased_schedule (S n) v (Some i) ≅
+    Guard (erased_schedule n (remove_pool v i) None).
+  Proof.
+    intro Hret.
+    unfold erased_schedule, forget_scheduler_offers.
+    rewrite unfold_interp.
+    rewrite (schedule_with_offers_focused_ret n v i Hret).
+    reflexivity.
+  Qed.
+
+  Local Lemma erased_focused_br_equ n
+      (v : pool E (S n)) (i : Fin.t (S n)) b k :
+    observe (v i) = BrF b k ->
+    erased_schedule (S n) v (Some i) ≅
+    Br b (fun j => Guard (erased_schedule (S n)
+      (replace_pool v i (k j)) (Some i))).
+  Proof.
+    intro Hbr.
+    unfold erased_schedule, forget_scheduler_offers.
+    rewrite unfold_interp.
+    rewrite (schedule_with_offers_focused_br n v i b k Hbr).
+    reflexivity.
+  Qed.
+
+  Local Lemma erased_focused_guard_equ n
+      (v : pool E (S n)) (i : Fin.t (S n)) t :
+    observe (v i) = GuardF t ->
+    erased_schedule (S n) v (Some i) ≅
+    Guard (erased_schedule (S n) (replace_pool v i t) (Some i)).
+  Proof.
+    intro Hguard.
+    unfold erased_schedule, forget_scheduler_offers.
+    rewrite unfold_interp.
+    rewrite (schedule_with_offers_focused_guard n v i t Hguard).
+    reflexivity.
+  Qed.
+
+  Local Lemma erased_focused_yield_equ n
+      (v : pool E (S n)) (i : Fin.t (S n)) k :
+    observe (v i) = VisF (inl Yield) k ->
+    erased_schedule (S n) v (Some i) ≅
+    Guard (erased_schedule (S n) (replace_pool v i (k tt)) None).
+  Proof.
+    intro Hyield.
+    unfold erased_schedule, forget_scheduler_offers.
+    rewrite unfold_interp.
+    rewrite (schedule_with_offers_focused_yield n v i k Hyield).
+    reflexivity.
+  Qed.
+
+  Local Lemma erased_focused_fork_equ n
+      (v : pool E (S n)) (i : Fin.t (S n)) k :
+    observe (v i) = VisF (inr (inl Fork)) k ->
+    erased_schedule (S n) v (Some i) ≅
+    Vis (inr (inl Spawn) : yieldE + (spawnE + E))
+      (fun _ => Guard (erased_schedule (S (S n))
+        (cons_pool (k true) (replace_pool v i (k false)))
+        (Some (Fin.FS i)))).
+  Proof.
+    intro Hfork.
+    unfold erased_schedule, forget_scheduler_offers.
+    rewrite unfold_interp.
+    rewrite (schedule_with_offers_focused_fork n v i k Hfork).
+    cbn.
+    unfold ICtree.trigger, resum, ReSum_refl, resum_ret,
+      ReSumRet_refl.
+    rewrite bind_vis.
+    setoid_rewrite bind_ret_l.
+    reflexivity.
+  Qed.
+
+  Local Lemma erased_focused_user_event_equ n
+      (v : pool E (S n)) (i : Fin.t (S n)) e k :
+    observe (v i) = VisF (inr (inr e)) k ->
+    erased_schedule (S n) v (Some i) ≅
+    Vis (inr (inr e) : yieldE + (spawnE + E))
+      (fun x => Guard (erased_schedule (S n)
+        (replace_pool v i (k x)) (Some i))).
+  Proof.
+    intro Huser.
+    unfold erased_schedule, forget_scheduler_offers.
+    rewrite unfold_interp.
+    rewrite (schedule_with_offers_focused_user_event n v i e k Huser).
+    cbn.
+    unfold ICtree.trigger, resum, ReSum_refl, resum_ret,
+      ReSumRet_refl.
+    rewrite bind_vis.
+    setoid_rewrite bind_ret_l.
+    reflexivity.
+  Qed.
+
+  Local Lemma schedule_focused_yield_equ n
+      (v : pool E (S n)) (i : Fin.t (S n)) k :
+    observe (v i) = VisF (inl Yield) k ->
+    schedule (S n) v (Some i) ≅
+    Guard (schedule (S n) (replace_pool v i (k tt)) None).
+  Proof.
+    intro Hyield.
+    rewrite (ictree_eta (schedule (S n) v (Some i))).
+    rewrite (schedule_focused_yield n v i k Hyield).
+    reflexivity.
+  Qed.
+
+  Local Lemma guard_residual_from_equ (actual target residual : completed') :
+    observe actual = GuardF residual ->
+    actual ≅ Guard target ->
+    residual ≅ target.
+  Proof.
+    intros Hobs Heq.
+    apply equ_guard_invE.
+    transitivity actual.
+    - rewrite (ictree_eta actual). rewrite Hobs. reflexivity.
+    - exact Heq.
+  Qed.
+
+  Local Ltac contradiction_from_shape_equ actual Hobs Heq :=
+    exfalso;
+    rewrite (ictree_eta actual) in Heq;
+    rewrite <- Hobs in Heq;
+    step in Heq; inversion Heq.
+
+  Local Lemma erased_schedule_match_left_empty
+      (R : rel completed' completed')
+      (Hch : forall m (w : pool E m) f,
+        stR R (erased_schedule m w f) (schedule m w f))
+      l actual t' (v : pool E 0) :
+    actual ≅ erased_schedule 0 v None ->
+    trans l actual t' ->
+    exists u', trans l (schedule 0 v None) u' /\ stR R t' u'.
+  Proof.
+    intros Hactual TRactual.
+    assert (Hproj : actual ~ Ret tt).
+    { rewrite Hactual.
+      unfold erased_schedule.
+      apply forget_scheduler_offers_empty_no_focus_projection. }
+    destruct (sbisim_trans actual _ t' l eq Hproj TRactual) as
+      [l' [mid [Hmid [Hl' Hsb]]]]. subst l'.
+    apply trans_ret_inv in Hmid as [Hmid ->].
+    exists stuck. split.
+    - rewrite (trans_schedule_empty_ret v). apply trans_ret.
+    - rewrite Hsb. rewrite Hmid. reflexivity.
+  Qed.
+
+  Local Lemma erased_schedule_match_left_no_focus
+      (R : rel completed' completed')
+      (Hch : forall m (w : pool E m) f,
+        stR R (erased_schedule m w f) (schedule m w f))
+      l actual t' n (v : pool E (S n)) :
+    actual ≅ erased_schedule (S n) v None ->
+    trans l actual t' ->
+    exists u', trans l (schedule (S n) v None) u' /\ stR R t' u'.
+  Proof.
+    intros Hactual TRactual.
+    assert (Hproj : actual ~
+      Vis (inl Yield : yieldE + (spawnE + E))
+        (fun _ : unit => Br n (fun i =>
+           erased_schedule (S n) v (Some i)))).
+    { rewrite Hactual.
+      unfold erased_schedule.
+      apply forget_scheduler_offers_no_focus_projection_to_focused. }
+    destruct (sbisim_trans actual _ t' l eq Hproj TRactual) as
+      [l' [mid [Hmid [Hl' Hsb]]]]. subst l'.
+    apply trans_vis_inv in Hmid as [x [Hmid Hlabel]].
+    subst l. destruct x.
+    exists (Br n (fun i => schedule (S n) v (Some i))). split.
+    - apply trans_schedule_no_focus_nonempty.
+    - rewrite Hsb. rewrite Hmid.
+      apply (coinduction.bt_t (sb eq)).
+      apply step_sb_br_id; [reflexivity | intro j].
+      apply Hch.
+  Qed.
+
+  Local Lemma erased_schedule_match_left_br
+      (R : rel completed' completed')
+      (Hch : forall m (w : pool E m) f,
+        stR R (erased_schedule m w f) (schedule m w f))
+      l actual t' n (v : pool E (S n)) (i : Fin.t (S n)) b k :
+    observe (v i) = BrF b k ->
+    actual ≅ erased_schedule (S n) v (Some i) ->
+    trans l actual t' ->
+    exists u', trans l (schedule (S n) v (Some i)) u' /\ stR R t' u'.
+  Proof.
+    intros Hvi Hactual TRactual.
+    assert (Hproj : actual ~
+      Br b (fun j => erased_schedule (S n)
+        (replace_pool v i (k j)) (Some i))).
+    { rewrite Hactual.
+      apply forget_scheduler_offers_focused_br_projection.
+      exact Hvi. }
+    destruct (sbisim_trans actual _ t' l eq Hproj TRactual) as
+      [l' [mid [Hmid [Hl' Hsb]]]]. subst l'.
+    apply trans_br_inv in Hmid as [j [Hmid Hlabel]].
+    subst l.
+    exists (schedule (S n) (replace_pool v i (k j)) (Some i)).
+    split.
+    - apply trans_schedule_focused_br. exact Hvi.
+    - rewrite Hsb. rewrite Hmid. apply Hch.
+  Qed.
+
+  Local Lemma erased_schedule_match_left_fork
+      (R : rel completed' completed')
+      (Hch : forall m (w : pool E m) f,
+        stR R (erased_schedule m w f) (schedule m w f))
+      l actual t' n (v : pool E (S n)) (i : Fin.t (S n)) k :
+    observe (v i) = VisF (inr (inl Fork)) k ->
+    actual ≅ erased_schedule (S n) v (Some i) ->
+    trans l actual t' ->
+    exists u', trans l (schedule (S n) v (Some i)) u' /\ stR R t' u'.
+  Proof.
+    intros Hvi Hactual TRactual.
+    assert (Hproj : actual ~
+      Vis (inr (inl Spawn) : yieldE + (spawnE + E))
+        (fun _ => erased_schedule (S (S n))
+          (cons_pool (k true) (replace_pool v i (k false)))
+          (Some (Fin.FS i)))).
+    { rewrite Hactual.
+      apply forget_scheduler_offers_focused_fork_projection.
+      exact Hvi. }
+    destruct (sbisim_trans actual _ t' l eq Hproj TRactual) as
+      [l' [mid [Hmid [Hl' Hsb]]]]. subst l'.
+    apply trans_vis_inv in Hmid as [x [Hmid Hlabel]].
+    subst l. destruct x.
+    exists (schedule (S (S n))
+      (cons_pool (k true) (replace_pool v i (k false)))
+      (Some (Fin.FS i))). split.
+    - apply trans_schedule_focused_fork. exact Hvi.
+    - rewrite Hsb. rewrite Hmid. apply Hch.
+  Qed.
+
+  Local Lemma erased_schedule_match_left_user
+      (R : rel completed' completed')
+      (Hch : forall m (w : pool E m) f,
+        stR R (erased_schedule m w f) (schedule m w f))
+      l actual t' n (v : pool E (S n)) (i : Fin.t (S n)) e k :
+    observe (v i) = VisF (inr (inr e)) k ->
+    actual ≅ erased_schedule (S n) v (Some i) ->
+    trans l actual t' ->
+    exists u', trans l (schedule (S n) v (Some i)) u' /\ stR R t' u'.
+  Proof.
+    intros Hvi Hactual TRactual.
+    assert (Hproj : actual ~
+      Vis (inr (inr e) : yieldE + (spawnE + E))
+        (fun x => erased_schedule (S n)
+          (replace_pool v i (k x)) (Some i))).
+    { rewrite Hactual.
+      apply forget_scheduler_offers_focused_user_event_projection.
+      exact Hvi. }
+    destruct (sbisim_trans actual _ t' l eq Hproj TRactual) as
+      [l' [mid [Hmid [Hl' Hsb]]]]. subst l'.
+    apply trans_vis_inv in Hmid as [x [Hmid Hlabel]].
+    subst l.
+    exists (schedule (S n) (replace_pool v i (k x)) (Some i)).
+    split.
+    - apply trans_schedule_focused_user_event. exact Hvi.
+    - rewrite Hsb. rewrite Hmid. apply Hch.
+  Qed.
+
+  Local Lemma schedule_focused_br_equ n
+      (v : pool E (S n)) (i : Fin.t (S n)) b k :
+    observe (v i) = BrF b k ->
+    schedule (S n) v (Some i) ≅
+    Br b (fun j => schedule (S n) (replace_pool v i (k j)) (Some i)).
+  Proof.
+    intro Hbr.
+    rewrite (ictree_eta (schedule (S n) v (Some i))).
+    rewrite (schedule_focused_br n v i b k Hbr).
+    reflexivity.
+  Qed.
+
+  Local Lemma schedule_focused_fork_equ n
+      (v : pool E (S n)) (i : Fin.t (S n)) k :
+    observe (v i) = VisF (inr (inl Fork)) k ->
+    schedule (S n) v (Some i) ≅
+    Vis (inr (inl Spawn) : yieldE + (spawnE + E))
+      (fun _ => schedule (S (S n))
+        (cons_pool (k true) (replace_pool v i (k false)))
+        (Some (Fin.FS i))).
+  Proof.
+    intro Hfork.
+    rewrite (ictree_eta (schedule (S n) v (Some i))).
+    rewrite (schedule_focused_fork n v i k Hfork).
+    reflexivity.
+  Qed.
+
+  Local Lemma schedule_focused_user_event_equ n
+      (v : pool E (S n)) (i : Fin.t (S n)) e k :
+    observe (v i) = VisF (inr (inr e)) k ->
+    schedule (S n) v (Some i) ≅
+    Vis (inr (inr e) : yieldE + (spawnE + E))
+      (fun x => schedule (S n) (replace_pool v i (k x)) (Some i)).
+  Proof.
+    intro Huser.
+    rewrite (ictree_eta (schedule (S n) v (Some i))).
+    rewrite (schedule_focused_user_event n v i e k Huser).
+    reflexivity.
+  Qed.
+
+  Local Lemma erased_schedule_match_right_empty
+      (R : rel completed' completed')
+      (Hch : forall m (w : pool E m) f,
+        stR R (erased_schedule m w f) (schedule m w f))
+      l actual t' (v : pool E 0) :
+    actual ≅ schedule 0 v None ->
+    trans l actual t' ->
+    exists u', trans l (erased_schedule 0 v None) u' /\ stR R u' t'.
+  Proof.
+    intros Hactual TRactual.
+    assert (Hret : actual ~ Ret tt).
+    { rewrite Hactual. rewrite (trans_schedule_empty_ret v). reflexivity. }
+    destruct (sbisim_trans actual _ t' l eq Hret TRactual) as
+      [l' [mid [Hmid [Hl' Hsb_mid]]]]. subst l'.
+    assert (Hproj : Ret tt ~ erased_schedule 0 v None).
+    { symmetry.
+      unfold erased_schedule.
+      apply forget_scheduler_offers_empty_no_focus_projection. }
+    destruct (sbisim_trans (Ret tt) _ mid l eq Hproj Hmid) as
+      [l'' [u' [Htru [Hl'' Hsb_u]]]]. subst l''.
+    exists u'. split.
+    - exact Htru.
+    - rewrite Hsb_mid. rewrite <- Hsb_u. reflexivity.
+  Qed.
+
+  Local Lemma erased_schedule_match_right_no_focus
+      (R : rel completed' completed')
+      (Hch : forall m (w : pool E m) f,
+        stR R (erased_schedule m w f) (schedule m w f))
+      l actual t' n (v : pool E (S n)) :
+    actual ≅ schedule (S n) v None ->
+    trans l actual t' ->
+    exists u', trans l (erased_schedule (S n) v None) u' /\ stR R u' t'.
+  Proof.
+    intros Hactual TRactual.
+    set (sres := Br n (fun i => schedule (S n) v (Some i))).
+    set (lres := Br n (fun i => erased_schedule (S n) v (Some i))).
+    assert (Hshape : actual ~
+      Vis (inl Yield : yieldE + (spawnE + E)) (fun _ : unit => sres)).
+    { rewrite Hactual. rewrite (schedule_no_focus_equ n v). reflexivity. }
+    destruct (sbisim_trans actual _ t' l eq Hshape TRactual) as
+      [l' [mid [Hmid [Hl' Hsb_mid]]]]. subst l'.
+    apply trans_vis_inv in Hmid as [x [Hmid Hlabel]].
+    subst l. destruct x.
+    assert (Hstep_lres : trans (obs (inl Yield : yieldE + (spawnE + E)) tt)
+      (Vis (inl Yield : yieldE + (spawnE + E)) (fun _ : unit => lres))
+      lres).
+    { apply trans_vis. }
+    assert (Hproj :
+      Vis (inl Yield : yieldE + (spawnE + E)) (fun _ : unit => lres) ~
+      erased_schedule (S n) v None).
+    { symmetry.
+      unfold erased_schedule.
+      apply forget_scheduler_offers_no_focus_projection_to_focused. }
+    destruct (sbisim_trans _ _ lres
+      (obs (inl Yield : yieldE + (spawnE + E)) tt) eq Hproj
+      Hstep_lres) as [l'' [u' [Htru [Hl'' Hsb_u]]]].
+    subst l''.
+    exists u'. split.
+    - exact Htru.
+    - rewrite Hsb_mid. rewrite Hmid. rewrite <- Hsb_u.
+      apply (coinduction.bt_t (sb eq)).
+      apply step_sb_br_id; [reflexivity | intro j].
+      apply Hch.
+  Qed.
+
+  Local Lemma erased_schedule_match_right_br
+      (R : rel completed' completed')
+      (Hch : forall m (w : pool E m) f,
+        stR R (erased_schedule m w f) (schedule m w f))
+      l actual t' n (v : pool E (S n)) (i : Fin.t (S n)) b k :
+    observe (v i) = BrF b k ->
+    actual ≅ schedule (S n) v (Some i) ->
+    trans l actual t' ->
+    exists u', trans l (erased_schedule (S n) v (Some i)) u' /\ stR R u' t'.
+  Proof.
+    intros Hvi Hactual TRactual.
+    set (sres := fun j =>
+      schedule (S n) (replace_pool v i (k j)) (Some i)).
+    set (lres := fun j =>
+      erased_schedule (S n) (replace_pool v i (k j)) (Some i)).
+    assert (Hshape : actual ~ Br b sres).
+    { rewrite Hactual. rewrite (schedule_focused_br_equ n v i b k Hvi).
+      reflexivity. }
+    destruct (sbisim_trans actual _ t' l eq Hshape TRactual) as
+      [l' [mid [Hmid [Hl' Hsb_mid]]]]. subst l'.
+    apply trans_br_inv in Hmid as [j [Hmid Hlabel]].
+    subst l.
+    assert (Hstep_lres : trans tau (Br b lres) (lres j)).
+    { apply trans_br with (x := j). reflexivity. }
+    assert (Hproj : Br b lres ~ erased_schedule (S n) v (Some i)).
+    { symmetry.
+      apply forget_scheduler_offers_focused_br_projection. exact Hvi. }
+    destruct (sbisim_trans _ _ (lres j) tau eq Hproj Hstep_lres)
+      as [l'' [u' [Htru [Hl'' Hsb_u]]]]. subst l''.
+    exists u'. split.
+    - exact Htru.
+    - rewrite Hsb_mid. rewrite Hmid. rewrite <- Hsb_u. apply Hch.
+  Qed.
+
+  Local Lemma erased_schedule_match_right_fork
+      (R : rel completed' completed')
+      (Hch : forall m (w : pool E m) f,
+        stR R (erased_schedule m w f) (schedule m w f))
+      l actual t' n (v : pool E (S n)) (i : Fin.t (S n)) k :
+    observe (v i) = VisF (inr (inl Fork)) k ->
+    actual ≅ schedule (S n) v (Some i) ->
+    trans l actual t' ->
+    exists u', trans l (erased_schedule (S n) v (Some i)) u' /\ stR R u' t'.
+  Proof.
+    intros Hvi Hactual TRactual.
+    set (sres := schedule (S (S n))
+      (cons_pool (k true) (replace_pool v i (k false)))
+      (Some (Fin.FS i))).
+    set (lres := erased_schedule (S (S n))
+      (cons_pool (k true) (replace_pool v i (k false)))
+      (Some (Fin.FS i))).
+    assert (Hshape : actual ~
+      Vis (inr (inl Spawn) : yieldE + (spawnE + E))
+        (fun _ : unit => sres)).
+    { rewrite Hactual. rewrite (schedule_focused_fork_equ n v i k Hvi).
+      reflexivity. }
+    destruct (sbisim_trans actual _ t' l eq Hshape TRactual) as
+      [l' [mid [Hmid [Hl' Hsb_mid]]]]. subst l'.
+    apply trans_vis_inv in Hmid as [x [Hmid Hlabel]].
+    subst l. destruct x.
+    assert (Hstep_lres : trans
+      (obs (inr (inl Spawn) : yieldE + (spawnE + E)) tt)
+      (Vis (inr (inl Spawn) : yieldE + (spawnE + E))
+        (fun _ : unit => lres)) lres).
+    { apply trans_vis. }
+    assert (Hproj :
+      Vis (inr (inl Spawn) : yieldE + (spawnE + E))
+        (fun _ : unit => lres) ~
+      erased_schedule (S n) v (Some i)).
+    { symmetry.
+      apply forget_scheduler_offers_focused_fork_projection. exact Hvi. }
+    destruct (sbisim_trans _ _ lres
+      (obs (inr (inl Spawn) : yieldE + (spawnE + E)) tt) eq Hproj
+      Hstep_lres) as [l'' [u' [Htru [Hl'' Hsb_u]]]].
+    subst l''.
+    exists u'. split.
+    - exact Htru.
+    - rewrite Hsb_mid. rewrite Hmid. rewrite <- Hsb_u. apply Hch.
+  Qed.
+
+  Local Lemma erased_schedule_match_right_user
+      (R : rel completed' completed')
+      (Hch : forall m (w : pool E m) f,
+        stR R (erased_schedule m w f) (schedule m w f))
+      l actual t' n (v : pool E (S n)) (i : Fin.t (S n)) e k :
+    observe (v i) = VisF (inr (inr e)) k ->
+    actual ≅ schedule (S n) v (Some i) ->
+    trans l actual t' ->
+    exists u', trans l (erased_schedule (S n) v (Some i)) u' /\ stR R u' t'.
+  Proof.
+    intros Hvi Hactual TRactual.
+    set (sres := fun x =>
+      schedule (S n) (replace_pool v i (k x)) (Some i)).
+    set (lres := fun x =>
+      erased_schedule (S n) (replace_pool v i (k x)) (Some i)).
+    assert (Hshape : actual ~
+      Vis (inr (inr e) : yieldE + (spawnE + E)) sres).
+    { rewrite Hactual.
+      rewrite (schedule_focused_user_event_equ n v i e k Hvi).
+      reflexivity. }
+    destruct (sbisim_trans actual _ t' l eq Hshape TRactual) as
+      [l' [mid [Hmid [Hl' Hsb_mid]]]]. subst l'.
+    apply trans_vis_inv in Hmid as [x [Hmid Hlabel]].
+    subst l.
+    assert (Hstep_lres : trans
+      (obs (inr (inr e) : yieldE + (spawnE + E)) x)
+      (Vis (inr (inr e) : yieldE + (spawnE + E)) lres) (lres x)).
+    { apply trans_vis. }
+    assert (Hproj : Vis (inr (inr e) : yieldE + (spawnE + E)) lres ~
+      erased_schedule (S n) v (Some i)).
+    { symmetry.
+      apply forget_scheduler_offers_focused_user_event_projection. exact Hvi. }
+    destruct (sbisim_trans _ _ (lres x)
+      (obs (inr (inr e) : yieldE + (spawnE + E)) x) eq Hproj
+      Hstep_lres) as [l'' [u' [Htru [Hl'' Hsb_u]]]].
+    subst l''.
+    exists u'. split.
+    - exact Htru.
+    - rewrite Hsb_mid. rewrite Hmid. rewrite <- Hsb_u. apply Hch.
+  Qed.
+
+  Local Lemma erased_schedule_match_left (R : rel completed' completed')
+      (Hch : forall m (w : pool E m) f,
+        stR R (erased_schedule m w f) (schedule m w f)) :
+    forall l os ot', trans_ l os ot' ->
+    forall actual n (v : pool E n) focus t',
+      os = observe actual ->
+      ot' = observe t' ->
+      actual ≅ erased_schedule n v focus ->
+      exists u', trans l (schedule n v focus) u' /\ stR R t' u'.
+  Proof.
+    intros l os ot' TR.
+    induction TR; intros actual nn v focus t' Hos Hot Hactual.
+    - destruct focus as [i |].
+      + destruct nn as [| n']; [inversion i |].
+        destruct (observe (v i)) as [r | b k | g | e k] eqn:Hvi.
+        * destruct r.
+          assert (Hguard : actual ≅
+            Guard (erased_schedule n' (remove_pool v i) None)).
+          { transitivity (erased_schedule (S n') v (Some i)).
+            - exact Hactual.
+            - apply erased_focused_ret_equ. exact Hvi. }
+          assert (Ht : t ≅ erased_schedule n' (remove_pool v i) None).
+          { eapply guard_residual_from_equ.
+            - symmetry. exact Hos.
+            - exact Hguard. }
+          destruct (IHTR t n' (remove_pool v i) None t'
+            eq_refl Hot Ht) as [u' [Htru Hres]].
+          exists u'. split.
+          -- rewrite (trans_schedule_focused_ret n' v i Hvi).
+             apply trans_guard. exact Htru.
+          -- exact Hres.
+        * assert (Hproj : actual ~
+            Br b (fun j => erased_schedule (S n')
+              (replace_pool v i (k j)) (Some i))).
+          { rewrite Hactual.
+            apply forget_scheduler_offers_focused_br_projection.
+            exact Hvi. }
+          assert (TRactual : trans l actual t').
+          { unfold trans. rewrite <- Hos, <- Hot. constructor. exact TR. }
+          destruct (sbisim_trans actual _ t' l eq Hproj TRactual) as
+            [l' [mid [Hmid [Hl' Hsb]]]]. subst l'.
+          apply trans_br_inv in Hmid as [j [Hmid ->]].
+          exists (schedule (S n') (replace_pool v i (k j)) (Some i)).
+          split.
+          -- apply trans_schedule_focused_br. exact Hvi.
+          -- rewrite Hsb. rewrite Hmid. apply Hch.
+        * assert (Hguard : actual ≅
+            Guard (erased_schedule (S n') (replace_pool v i g) (Some i))).
+          { transitivity (erased_schedule (S n') v (Some i)).
+            - exact Hactual.
+            - apply erased_focused_guard_equ. exact Hvi. }
+          assert (Ht : t ≅
+            erased_schedule (S n') (replace_pool v i g) (Some i)).
+          { eapply guard_residual_from_equ.
+            - symmetry. exact Hos.
+            - exact Hguard. }
+          destruct (IHTR t (S n') (replace_pool v i g) (Some i) t'
+            eq_refl Hot Ht) as [u' [Htru Hres]].
+          exists u'. split.
+          -- rewrite (trans_schedule_focused_guard n' v i g Hvi).
+             apply trans_guard. exact Htru.
+          -- exact Hres.
+        * destruct e as [yld | [frk | usr]].
+          -- destruct yld.
+             assert (Hguard : actual ≅
+               Guard (erased_schedule (S n')
+                 (replace_pool v i (k tt)) None)).
+             { transitivity (erased_schedule (S n') v (Some i)).
+               - exact Hactual.
+               - apply erased_focused_yield_equ. exact Hvi. }
+             assert (Ht : t ≅ erased_schedule (S n')
+               (replace_pool v i (k tt)) None).
+             { eapply guard_residual_from_equ.
+               - symmetry. exact Hos.
+               - exact Hguard. }
+             destruct (IHTR t (S n') (replace_pool v i (k tt)) None t'
+               eq_refl Hot Ht) as [u' [Htru Hres]].
+             exists u'. split.
+             ++ rewrite (schedule_focused_yield_equ n' v i k Hvi).
+                apply trans_guard. exact Htru.
+             ++ exact Hres.
+          -- destruct frk.
+             assert (Hproj : actual ~
+               Vis (inr (inl Spawn) : yieldE + (spawnE + E))
+                 (fun _ => erased_schedule (S (S n'))
+                   (cons_pool (k true) (replace_pool v i (k false)))
+                   (Some (Fin.FS i)))).
+             { rewrite Hactual.
+               apply forget_scheduler_offers_focused_fork_projection.
+               exact Hvi. }
+             assert (TRactual : trans l actual t').
+             { unfold trans. rewrite <- Hos, <- Hot. constructor. exact TR. }
+             destruct (sbisim_trans actual _ t' l eq Hproj TRactual) as
+               [l' [mid [Hmid [Hl' Hsb]]]]. subst l'.
+             apply trans_vis_inv in Hmid as [x [Hmid ->]].
+             destruct x.
+             exists (schedule (S (S n'))
+               (cons_pool (k true) (replace_pool v i (k false)))
+               (Some (Fin.FS i))). split.
+             ++ apply trans_schedule_focused_fork. exact Hvi.
+             ++ rewrite Hsb. rewrite Hmid. apply Hch.
+          -- assert (Hproj : actual ~
+               Vis (inr (inr usr) : yieldE + (spawnE + E))
+                 (fun x => erased_schedule (S n')
+                   (replace_pool v i (k x)) (Some i))).
+             { rewrite Hactual.
+               apply forget_scheduler_offers_focused_user_event_projection.
+               exact Hvi. }
+             assert (TRactual : trans l actual t').
+             { unfold trans. rewrite <- Hos, <- Hot. constructor. exact TR. }
+             destruct (sbisim_trans actual _ t' l eq Hproj TRactual) as
+               [l' [mid [Hmid [Hl' Hsb]]]]. subst l'.
+             apply trans_vis_inv in Hmid as [x [Hmid ->]].
+             exists (schedule (S n') (replace_pool v i (k x)) (Some i)).
+             split.
+             ++ apply trans_schedule_focused_user_event. exact Hvi.
+             ++ rewrite Hsb. rewrite Hmid. apply Hch.
+      + destruct nn as [| n'].
+        * assert (Hproj : actual ~ Ret tt).
+          { rewrite Hactual.
+            unfold erased_schedule.
+            apply forget_scheduler_offers_empty_no_focus_projection. }
+          assert (TRactual : trans l actual t').
+          { unfold trans. rewrite <- Hos, <- Hot. constructor. exact TR. }
+          destruct (sbisim_trans actual _ t' l eq Hproj TRactual) as
+            [l' [mid [Hmid [Hl' Hsb]]]]. subst l'.
+          apply trans_ret_inv in Hmid as [Hmid ->].
+          exists stuck. split.
+          -- rewrite (trans_schedule_empty_ret v). apply trans_ret.
+          -- rewrite Hsb. rewrite Hmid. reflexivity.
+        * assert (Hproj : actual ~
+            Vis (inl Yield : yieldE + (spawnE + E))
+              (fun _ : unit => Br n' (fun i =>
+                 erased_schedule (S n') v (Some i)))).
+          { rewrite Hactual.
+            unfold erased_schedule.
+            apply forget_scheduler_offers_no_focus_projection_to_focused. }
+          assert (TRactual : trans l actual t').
+          { unfold trans. rewrite <- Hos, <- Hot. constructor. exact TR. }
+          destruct (sbisim_trans actual _ t' l eq Hproj TRactual) as
+            [l' [mid [Hmid [Hl' Hsb]]]]. subst l'.
+          apply trans_vis_inv in Hmid as [x [Hmid ->]].
+          destruct x.
+          exists (Br n' (fun i => schedule (S n') v (Some i))). split.
+          -- apply trans_schedule_no_focus_nonempty.
+          -- rewrite Hsb. rewrite Hmid.
+             apply (coinduction.bt_t (sb eq)).
+             apply step_sb_br_id; [reflexivity | intro j].
+             apply Hch.
+    - assert (TRactual : trans tau actual t').
+      { unfold trans. rewrite <- Hos, <- Hot.
+        eapply Steptau. exact H0. }
+      destruct focus as [i |].
+      + destruct nn as [| n']; [inversion i |].
+        destruct (observe (v i)) as [r | b k0 | g | e k0] eqn:Hvi.
+        * destruct r.
+          assert (Hguard : actual ≅
+            Guard (erased_schedule n' (remove_pool v i) None)).
+          { transitivity (erased_schedule (S n') v (Some i)).
+            - exact Hactual.
+            - apply erased_focused_ret_equ. exact Hvi. }
+          contradiction_from_shape_equ actual Hos Hguard.
+        * eapply erased_schedule_match_left_br; eauto.
+        * assert (Hguard : actual ≅
+            Guard (erased_schedule (S n') (replace_pool v i g) (Some i))).
+          { transitivity (erased_schedule (S n') v (Some i)).
+            - exact Hactual.
+            - apply erased_focused_guard_equ. exact Hvi. }
+          contradiction_from_shape_equ actual Hos Hguard.
+        * destruct e as [yld | [frk | usr]].
+          -- destruct yld.
+             assert (Hguard : actual ≅
+               Guard (erased_schedule (S n')
+                 (replace_pool v i (k0 tt)) None)).
+             { transitivity (erased_schedule (S n') v (Some i)).
+               - exact Hactual.
+               - apply erased_focused_yield_equ. exact Hvi. }
+             contradiction_from_shape_equ actual Hos Hguard.
+          -- destruct frk.
+             assert (Hvis : actual ≅
+               Vis (inr (inl Spawn) : yieldE + (spawnE + E))
+                 (fun _ => Guard (erased_schedule (S (S n'))
+                   (cons_pool (k0 true) (replace_pool v i (k0 false)))
+                   (Some (Fin.FS i))))).
+             { transitivity (erased_schedule (S n') v (Some i)).
+               - exact Hactual.
+               - apply erased_focused_fork_equ. exact Hvi. }
+             contradiction_from_shape_equ actual Hos Hvis.
+          -- assert (Hvis : actual ≅
+               Vis (inr (inr usr) : yieldE + (spawnE + E))
+                 (fun x => Guard (erased_schedule (S n')
+                   (replace_pool v i (k0 x)) (Some i)))).
+             { transitivity (erased_schedule (S n') v (Some i)).
+               - exact Hactual.
+               - apply erased_focused_user_event_equ. exact Hvi. }
+             contradiction_from_shape_equ actual Hos Hvis.
+      + destruct nn as [| n'].
+        * eapply erased_schedule_match_left_empty; eauto.
+        * eapply erased_schedule_match_left_no_focus; eauto.
+    - assert (TRactual : trans (obs e x) actual t').
+      { unfold trans. rewrite <- Hos, <- Hot.
+        eapply Stepobs. exact H0. }
+      destruct focus as [i |].
+      + destruct nn as [| n']; [inversion i |].
+        destruct (observe (v i)) as [r | b k0 | g | e0 k0] eqn:Hvi.
+        * destruct r.
+          assert (Hguard : actual ≅
+            Guard (erased_schedule n' (remove_pool v i) None)).
+          { transitivity (erased_schedule (S n') v (Some i)).
+            - exact Hactual.
+            - apply erased_focused_ret_equ. exact Hvi. }
+          contradiction_from_shape_equ actual Hos Hguard.
+        * assert (Hbr : actual ≅
+            Br b (fun j => Guard (erased_schedule (S n')
+              (replace_pool v i (k0 j)) (Some i)))).
+          { transitivity (erased_schedule (S n') v (Some i)).
+            - exact Hactual.
+            - apply erased_focused_br_equ. exact Hvi. }
+          contradiction_from_shape_equ actual Hos Hbr.
+        * assert (Hguard : actual ≅
+            Guard (erased_schedule (S n') (replace_pool v i g) (Some i))).
+          { transitivity (erased_schedule (S n') v (Some i)).
+            - exact Hactual.
+            - apply erased_focused_guard_equ. exact Hvi. }
+          contradiction_from_shape_equ actual Hos Hguard.
+        * destruct e0 as [yld | [frk | usr]].
+          -- destruct yld.
+             assert (Hguard : actual ≅
+               Guard (erased_schedule (S n')
+                 (replace_pool v i (k0 tt)) None)).
+             { transitivity (erased_schedule (S n') v (Some i)).
+               - exact Hactual.
+               - apply erased_focused_yield_equ. exact Hvi. }
+             contradiction_from_shape_equ actual Hos Hguard.
+          -- destruct frk.
+             eapply erased_schedule_match_left_fork; eauto.
+          -- eapply erased_schedule_match_left_user; eauto.
+      + destruct nn as [| n'].
+        * eapply erased_schedule_match_left_empty; eauto.
+        * eapply erased_schedule_match_left_no_focus; eauto.
+    - assert (TRactual : trans (val r) actual t').
+      { unfold trans. rewrite <- Hos, <- Hot.
+        eapply Stepval. exact H0. }
+      destruct focus as [i |].
+      + destruct nn as [| n']; [inversion i |].
+        destruct (observe (v i)) as [r0 | b k0 | g | e k0] eqn:Hvi.
+        * destruct r0.
+          assert (Hguard : actual ≅
+            Guard (erased_schedule n' (remove_pool v i) None)).
+          { transitivity (erased_schedule (S n') v (Some i)).
+            - exact Hactual.
+            - apply erased_focused_ret_equ. exact Hvi. }
+          contradiction_from_shape_equ actual Hos Hguard.
+        * assert (Hbr : actual ≅
+            Br b (fun j => Guard (erased_schedule (S n')
+              (replace_pool v i (k0 j)) (Some i)))).
+          { transitivity (erased_schedule (S n') v (Some i)).
+            - exact Hactual.
+            - apply erased_focused_br_equ. exact Hvi. }
+          contradiction_from_shape_equ actual Hos Hbr.
+        * assert (Hguard : actual ≅
+            Guard (erased_schedule (S n') (replace_pool v i g) (Some i))).
+          { transitivity (erased_schedule (S n') v (Some i)).
+            - exact Hactual.
+            - apply erased_focused_guard_equ. exact Hvi. }
+          contradiction_from_shape_equ actual Hos Hguard.
+        * destruct e as [yld | [frk | usr]].
+          -- destruct yld.
+             assert (Hguard : actual ≅
+               Guard (erased_schedule (S n')
+                 (replace_pool v i (k0 tt)) None)).
+             { transitivity (erased_schedule (S n') v (Some i)).
+               - exact Hactual.
+               - apply erased_focused_yield_equ. exact Hvi. }
+             contradiction_from_shape_equ actual Hos Hguard.
+          -- destruct frk.
+             assert (Hvis : actual ≅
+               Vis (inr (inl Spawn) : yieldE + (spawnE + E))
+                 (fun _ => Guard (erased_schedule (S (S n'))
+                   (cons_pool (k0 true) (replace_pool v i (k0 false)))
+                   (Some (Fin.FS i))))).
+             { transitivity (erased_schedule (S n') v (Some i)).
+               - exact Hactual.
+               - apply erased_focused_fork_equ. exact Hvi. }
+             contradiction_from_shape_equ actual Hos Hvis.
+          -- assert (Hvis : actual ≅
+               Vis (inr (inr usr) : yieldE + (spawnE + E))
+                 (fun x => Guard (erased_schedule (S n')
+                   (replace_pool v i (k0 x)) (Some i)))).
+             { transitivity (erased_schedule (S n') v (Some i)).
+               - exact Hactual.
+               - apply erased_focused_user_event_equ. exact Hvi. }
+             contradiction_from_shape_equ actual Hos Hvis.
+      + destruct nn as [| n'].
+        * eapply erased_schedule_match_left_empty; eauto.
+        * eapply erased_schedule_match_left_no_focus; eauto.
+  Qed.
+
+  Local Lemma erased_schedule_match_right (R : rel completed' completed')
+      (Hch : forall m (w : pool E m) f,
+        stR R (erased_schedule m w f) (schedule m w f)) :
+    forall l os ot', trans_ l os ot' ->
+    forall actual n (v : pool E n) focus t',
+      os = observe actual ->
+      ot' = observe t' ->
+      actual ≅ schedule n v focus ->
+      exists u', trans l (erased_schedule n v focus) u' /\ stR R u' t'.
+  Proof.
+    intros l os ot' TR.
+    induction TR; intros actual nn v focus t' Hos Hot Hactual.
+    - assert (TRactual : trans l actual t').
+      { unfold trans. rewrite <- Hos, <- Hot. constructor. exact TR. }
+      destruct focus as [i |].
+      + destruct nn as [| n']; [inversion i |].
+        destruct (observe (v i)) as [r | b k | g | e k] eqn:Hvi.
+        * destruct r.
+          assert (Hguard : actual ≅
+            Guard (schedule n' (remove_pool v i) None)).
+          { transitivity (schedule (S n') v (Some i)).
+            - exact Hactual.
+            - apply trans_schedule_focused_ret. exact Hvi. }
+          assert (Ht : t ≅ schedule n' (remove_pool v i) None).
+          { eapply guard_residual_from_equ.
+            - symmetry. exact Hos.
+            - exact Hguard. }
+          destruct (IHTR t n' (remove_pool v i) None t'
+            eq_refl Hot Ht) as [u' [Htru Hres]].
+          exists u'. split.
+          -- rewrite (erased_focused_ret_equ n' v i Hvi).
+             apply trans_guard. exact Htru.
+          -- exact Hres.
+        * eapply erased_schedule_match_right_br; eauto.
+        * assert (Hguard : actual ≅
+            Guard (schedule (S n') (replace_pool v i g) (Some i))).
+          { transitivity (schedule (S n') v (Some i)).
+            - exact Hactual.
+            - apply trans_schedule_focused_guard. exact Hvi. }
+          assert (Ht : t ≅
+            schedule (S n') (replace_pool v i g) (Some i)).
+          { eapply guard_residual_from_equ.
+            - symmetry. exact Hos.
+            - exact Hguard. }
+          destruct (IHTR t (S n') (replace_pool v i g) (Some i) t'
+            eq_refl Hot Ht) as [u' [Htru Hres]].
+          exists u'. split.
+          -- rewrite (erased_focused_guard_equ n' v i g Hvi).
+             apply trans_guard. exact Htru.
+          -- exact Hres.
+        * destruct e as [yld | [frk | usr]].
+          -- destruct yld.
+             assert (Hguard : actual ≅
+               Guard (schedule (S n')
+                 (replace_pool v i (k tt)) None)).
+             { transitivity (schedule (S n') v (Some i)).
+               - exact Hactual.
+               - apply schedule_focused_yield_equ. exact Hvi. }
+             assert (Ht : t ≅ schedule (S n')
+               (replace_pool v i (k tt)) None).
+             { eapply guard_residual_from_equ.
+               - symmetry. exact Hos.
+               - exact Hguard. }
+             destruct (IHTR t (S n') (replace_pool v i (k tt)) None t'
+               eq_refl Hot Ht) as [u' [Htru Hres]].
+             exists u'. split.
+             ++ rewrite (erased_focused_yield_equ n' v i k Hvi).
+                apply trans_guard. exact Htru.
+             ++ exact Hres.
+          -- destruct frk.
+             eapply erased_schedule_match_right_fork; eauto.
+          -- eapply erased_schedule_match_right_user; eauto.
+      + destruct nn as [| n'].
+        * eapply erased_schedule_match_right_empty; eauto.
+        * eapply erased_schedule_match_right_no_focus; eauto.
+    - assert (TRactual : trans tau actual t').
+      { unfold trans. rewrite <- Hos, <- Hot.
+        eapply Steptau. exact H0. }
+      destruct focus as [i |].
+      + destruct nn as [| n']; [inversion i |].
+        destruct (observe (v i)) as [r | b k0 | g | e k0] eqn:Hvi.
+        * destruct r.
+          assert (Hguard : actual ≅
+            Guard (schedule n' (remove_pool v i) None)).
+          { transitivity (schedule (S n') v (Some i)).
+            - exact Hactual.
+            - apply trans_schedule_focused_ret. exact Hvi. }
+          contradiction_from_shape_equ actual Hos Hguard.
+        * eapply erased_schedule_match_right_br; eauto.
+        * assert (Hguard : actual ≅
+            Guard (schedule (S n') (replace_pool v i g) (Some i))).
+          { transitivity (schedule (S n') v (Some i)).
+            - exact Hactual.
+            - apply trans_schedule_focused_guard. exact Hvi. }
+          contradiction_from_shape_equ actual Hos Hguard.
+        * destruct e as [yld | [frk | usr]].
+          -- destruct yld.
+             assert (Hguard : actual ≅
+               Guard (schedule (S n')
+                 (replace_pool v i (k0 tt)) None)).
+             { transitivity (schedule (S n') v (Some i)).
+               - exact Hactual.
+               - apply schedule_focused_yield_equ. exact Hvi. }
+             contradiction_from_shape_equ actual Hos Hguard.
+          -- destruct frk.
+             eapply erased_schedule_match_right_fork; eauto.
+          -- eapply erased_schedule_match_right_user; eauto.
+      + destruct nn as [| n'].
+        * eapply erased_schedule_match_right_empty; eauto.
+        * eapply erased_schedule_match_right_no_focus; eauto.
+    - assert (TRactual : trans (obs e x) actual t').
+      { unfold trans. rewrite <- Hos, <- Hot.
+        eapply Stepobs. exact H0. }
+      destruct focus as [i |].
+      + destruct nn as [| n']; [inversion i |].
+        destruct (observe (v i)) as [r | b k0 | g | e0 k0] eqn:Hvi.
+        * destruct r.
+          assert (Hguard : actual ≅
+            Guard (schedule n' (remove_pool v i) None)).
+          { transitivity (schedule (S n') v (Some i)).
+            - exact Hactual.
+            - apply trans_schedule_focused_ret. exact Hvi. }
+          contradiction_from_shape_equ actual Hos Hguard.
+        * eapply erased_schedule_match_right_br; eauto.
+        * assert (Hguard : actual ≅
+            Guard (schedule (S n') (replace_pool v i g) (Some i))).
+          { transitivity (schedule (S n') v (Some i)).
+            - exact Hactual.
+            - apply trans_schedule_focused_guard. exact Hvi. }
+          contradiction_from_shape_equ actual Hos Hguard.
+        * destruct e0 as [yld | [frk | usr]].
+          -- destruct yld.
+             assert (Hguard : actual ≅
+               Guard (schedule (S n')
+                 (replace_pool v i (k0 tt)) None)).
+             { transitivity (schedule (S n') v (Some i)).
+               - exact Hactual.
+               - apply schedule_focused_yield_equ. exact Hvi. }
+             contradiction_from_shape_equ actual Hos Hguard.
+          -- destruct frk.
+             eapply erased_schedule_match_right_fork; eauto.
+          -- eapply erased_schedule_match_right_user; eauto.
+      + destruct nn as [| n'].
+        * eapply erased_schedule_match_right_empty; eauto.
+        * eapply erased_schedule_match_right_no_focus; eauto.
+    - assert (TRactual : trans (val r) actual t').
+      { unfold trans. rewrite <- Hos, <- Hot.
+        eapply Stepval. exact H0. }
+      destruct focus as [i |].
+      + destruct nn as [| n']; [inversion i |].
+        destruct (observe (v i)) as [r0 | b k0 | g | e k0] eqn:Hvi.
+        * destruct r0.
+          assert (Hguard : actual ≅
+            Guard (schedule n' (remove_pool v i) None)).
+          { transitivity (schedule (S n') v (Some i)).
+            - exact Hactual.
+            - apply trans_schedule_focused_ret. exact Hvi. }
+          contradiction_from_shape_equ actual Hos Hguard.
+        * eapply erased_schedule_match_right_br; eauto.
+        * assert (Hguard : actual ≅
+            Guard (schedule (S n') (replace_pool v i g) (Some i))).
+          { transitivity (schedule (S n') v (Some i)).
+            - exact Hactual.
+            - apply trans_schedule_focused_guard. exact Hvi. }
+          contradiction_from_shape_equ actual Hos Hguard.
+        * destruct e as [yld | [frk | usr]].
+          -- destruct yld.
+             assert (Hguard : actual ≅
+               Guard (schedule (S n')
+                 (replace_pool v i (k0 tt)) None)).
+             { transitivity (schedule (S n') v (Some i)).
+               - exact Hactual.
+               - apply schedule_focused_yield_equ. exact Hvi. }
+             contradiction_from_shape_equ actual Hos Hguard.
+          -- destruct frk.
+             eapply erased_schedule_match_right_fork; eauto.
+          -- eapply erased_schedule_match_right_user; eauto.
+      + destruct nn as [| n'].
+        * eapply erased_schedule_match_right_empty; eauto.
+        * eapply erased_schedule_match_right_no_focus; eauto.
+  Qed.
+
+  Theorem forget_scheduler_offers_preserves_schedule
+      n (v : pool E n) focus :
+    forget_scheduler_offers (schedule_with_offers n v focus) ~
+    schedule n v focus.
+  Proof.
+    change (erased_schedule n v focus ~ schedule n v focus).
+    revert n v focus.
+    coinduction R CH.
+    intros n v focus.
+    assert (Hch : forall m (w : pool E m) f,
+      stR R (erased_schedule m w f) (schedule m w f)).
+    { intros m w f. apply CH. }
+    split.
+    - intros l t' TR.
+      destruct (erased_schedule_match_left R Hch _ _ _ TR
+        (erased_schedule n v focus) n v focus t'
+        eq_refl eq_refl ltac:(reflexivity)) as [u' [Htru Hres]].
+      exists l, u'. split; [exact Htru | split].
+      + exact Hres.
+      + reflexivity.
+    - intros l t' TR.
+      destruct (erased_schedule_match_right R Hch _ _ _ TR
+        (schedule n v focus) n v focus t'
+        eq_refl eq_refl ltac:(reflexivity)) as [u' [Htru Hres]].
+      exists l, u'. split; [exact Htru | split].
+      + unfold Basics.flip. exact Hres.
+      + reflexivity.
+  Qed.
+
+  Record ReturnSlotTransport {n : nat}
+      (v : pool E (S n)) (removed : LiveSlot (S n))
+      (v' : pool E n) : Prop := {
+    return_new_slots_come_from_old_survivors :
+      forall j_new : LiveSlot n,
+        exists j_old : LiveSlot (S n),
+          j_old <> removed /\ v' j_new = v j_old;
+    return_old_survivors_reappear :
+      forall j_old : LiveSlot (S n),
+        j_old <> removed ->
+        exists j_new : LiveSlot n, v' j_new = v j_old
+  }.
+
+  Theorem return_removes_live_slot n
+      (v : pool E (S n)) (i : Fin.t (S n)) :
+    observe (v i) = RetF tt ->
+    ReturnSlotTransport v i (remove_pool v i).
+  Proof.
+    intro Hret; clear Hret.
+    revert v i.
+    induction n as [| n IH]; intros v i.
+    - constructor.
+      + intro j_new.
+        exact (Fin.case0 (fun j_new => exists j_old : LiveSlot 1,
+          j_old <> i /\ remove_pool v i j_new = v j_old) j_new).
+      + intros j_old Hneq.
+        contradiction Hneq. apply live_slot_one_eq.
+    - refine (Fin.caseS' i
+        (fun i => ReturnSlotTransport v i (remove_pool v i)) _ _).
+      + constructor.
+        * intro j_new.
+          exists (Fin.FS j_new). split.
+          -- discriminate.
+          -- reflexivity.
+        * intros j_old Hneq.
+          refine (Fin.caseS' j_old
+            (fun j => j <> Fin.F1 ->
+              exists j_new : LiveSlot (S n),
+                remove_pool v Fin.F1 j_new = v j) _ _ Hneq).
+          -- intro Hcontra. contradiction Hcontra; reflexivity.
+          -- intros j_new _. exists j_new. reflexivity.
+      + intro i_tail.
+        pose proof (IH (fun k => v (Fin.FS k)) i_tail) as IHt.
+        destruct IHt as [IHnew IHold].
+        constructor.
+        * intro j_new.
+          refine (Fin.caseS' j_new
+            (fun j => exists j_old : LiveSlot (S (S n)),
+              j_old <> Fin.FS i_tail /\
+              remove_pool v (Fin.FS i_tail) j = v j_old) _ _).
+          -- exists Fin.F1. split.
+             ++ discriminate.
+             ++ reflexivity.
+          -- intros j_new'.
+             destruct (IHnew j_new') as [j_old [Hneq Hv]].
+             exists (Fin.FS j_old). split.
+             ++ intro Heq. apply Fin.FS_inj in Heq.
+                contradiction Hneq.
+             ++ cbn. rewrite !fin_cast_refl. exact Hv.
+        * intros j_old Hneq.
+          refine (Fin.caseS' j_old
+            (fun j => j <> Fin.FS i_tail ->
+              exists j_new : LiveSlot (S n),
+                remove_pool v (Fin.FS i_tail) j_new = v j) _ _ Hneq).
+          -- intros _. exists Fin.F1. reflexivity.
+          -- intros j_old' Hneq'.
+             assert (Hsurv : j_old' <> i_tail) by
+               (intro Heq; subst; apply Hneq'; reflexivity).
+             destruct (IHold j_old' Hsurv) as [j_new Hv].
+             exists (Fin.FS j_new).
+             cbn. rewrite !fin_cast_refl. exact Hv.
+  Qed.
+
+  Definition shift_live_slot_across_spawn {n : nat}
+      (i : LiveSlot n) : LiveSlot (S n) :=
+    Fin.FS i.
+
+  Lemma shift_live_slot_across_spawn_head {n}
+      (child : thread E) (v : pool E n) :
+    cons_pool child v Fin.F1 = child.
+  Proof. apply cons_pool_head. Qed.
+
+  Lemma shift_live_slot_across_spawn_tail {n}
+      (child : thread E) (v : pool E n) (i : LiveSlot n) :
+    cons_pool child v (shift_live_slot_across_spawn i) = v i.
+  Proof. apply cons_pool_tail. Qed.
+
+  Lemma shift_live_slot_across_spawn_parent_slot n
+      (v : pool E (S n)) (i : LiveSlot (S n)) k :
+    cons_pool (k true) (replace_pool v i (k false))
+      (shift_live_slot_across_spawn i) = k false.
+  Proof.
+    rewrite shift_live_slot_across_spawn_tail.
+    apply replace_pool_hit.
+  Qed.
+
+  Lemma shift_live_slot_across_spawn_other_slot n
+      (v : pool E (S n)) (i j : LiveSlot (S n)) k :
+    i <> j ->
+    cons_pool (k true) (replace_pool v i (k false))
+      (shift_live_slot_across_spawn j) = v j.
+  Proof.
+    intro Hneq.
+    rewrite shift_live_slot_across_spawn_tail.
+    now apply replace_pool_miss.
+  Qed.
+
+  Lemma transport_live_slots_across_spawn_head {n}
+      (child : thread E) (v : pool E n) :
+    cons_pool child v Fin.F1 = child.
+  Proof. apply shift_live_slot_across_spawn_head. Qed.
+
+  Lemma transport_live_slots_across_spawn_tail {n}
+      (child : thread E) (v : pool E n) (i : LiveSlot n) :
+    cons_pool child v (shift_live_slot_across_spawn i) = v i.
+  Proof. apply shift_live_slot_across_spawn_tail. Qed.
+
+  Lemma transport_live_slots_across_spawn_parent_slot n
+      (v : pool E (S n)) (i : LiveSlot (S n)) k :
+    cons_pool (k true) (replace_pool v i (k false))
+      (shift_live_slot_across_spawn i) = k false.
+  Proof. apply shift_live_slot_across_spawn_parent_slot. Qed.
+
+  Lemma transport_live_slots_across_spawn_other_slot n
+      (v : pool E (S n)) (i j : LiveSlot (S n)) k :
+    i <> j ->
+    cons_pool (k true) (replace_pool v i (k false))
+      (shift_live_slot_across_spawn j) = v j.
+  Proof. apply shift_live_slot_across_spawn_other_slot. Qed.
+
+  Record SpawnSlotTransport {n : nat}
+      (v : pool E (S n)) (parent : LiveSlot (S n))
+      (k : bool -> thread E) (spawned : pool E (S (S n))) : Prop := {
+    spawn_child_at_head : spawned Fin.F1 = k true;
+    spawn_parent_at_shifted_slot : spawned (Fin.FS parent) = k false;
+    spawn_other_old_slots_shifted :
+      forall j : LiveSlot (S n),
+        j <> parent -> spawned (Fin.FS j) = v j
+  }.
+
+  Theorem transport_live_slots_across_spawn n
+      (v : pool E (S n)) (i : LiveSlot (S n)) k :
+    observe (v i) = VisF (inr (inl Fork)) k ->
+    SpawnSlotTransport v i k
+      (cons_pool (k true) (replace_pool v i (k false))).
+  Proof.
+    intro Hfork; clear Hfork.
+    constructor.
+    - apply cons_pool_head.
+    - rewrite cons_pool_tail. apply replace_pool_hit.
+    - intros j Hneq.
+      rewrite cons_pool_tail.
+      apply replace_pool_miss. congruence.
+  Qed.
+
+  Inductive offered_in_scheduler_prefix (n : nat) (i : LiveSlot n)
+      : observed_completed E -> Prop :=
+  | offered_prefix_here t k :
+      observe t = VisF (inl (ObsOffered (live_slot_ref i))) k ->
+      offered_in_scheduler_prefix n i t
+  | offered_prefix_later t obs k :
+      observe t = VisF (inl obs) k ->
+      offered_in_scheduler_prefix n i (k tt) ->
+      offered_in_scheduler_prefix n i t.
+
+  Lemma emit_live_slot_offers_into_then_offers m :
+    forall n (embed : LiveSlot n -> LiveSlot m) k (i : LiveSlot n),
+      offered_in_scheduler_prefix m (embed i)
+        (emit_live_slot_offers_into_then m n embed k).
+  Proof.
+    intros n embed k i.
+    induction i as [n' | n' i IH].
+    - apply offered_prefix_here with
+        (k := fun _ : unit =>
+          emit_live_slot_offers_into_then m n'
+            (fun i => embed (Fin.FS i)) k).
+      reflexivity.
+    - apply offered_prefix_later with
+        (obs := ObsOffered (live_slot_ref (embed Fin.F1)))
+        (k := fun _ : unit =>
+          emit_live_slot_offers_into_then m n'
+            (fun j => embed (Fin.FS j)) k).
+      + reflexivity.
+      + apply (IH (fun j => embed (Fin.FS j))).
+  Qed.
+
+  Lemma emit_live_slot_offers_then_offers n k (i : LiveSlot n) :
+    offered_in_scheduler_prefix n i (emit_live_slot_offers_then n k).
+  Proof.
+    unfold emit_live_slot_offers_then.
+    apply (emit_live_slot_offers_into_then_offers n n (fun i => i) k i).
+  Qed.
+
+  Lemma emit_live_slot_offers_offers n (i : LiveSlot n) :
+    offered_in_scheduler_prefix n i (emit_live_slot_offers n).
+  Proof.
+    apply emit_live_slot_offers_then_offers.
+  Qed.
+
+  Lemma emit_live_slot_offers_contains_every_slot n (i : LiveSlot n) :
+    offered_in_scheduler_prefix n i (emit_live_slot_offers n).
+  Proof.
+    apply emit_live_slot_offers_offers.
+  Qed.
+
+  Lemma schedule_with_offers_offer_prefix_offers m :
+    forall n (embed : LiveSlot n -> LiveSlot m) (v : pool E m)
+      (i : LiveSlot n),
+      offered_in_scheduler_prefix m (embed i)
+        (schedule_with_offers_offer_prefix m n embed v).
+  Proof.
+    intros n embed v i.
+    induction i as [n' | n' i IH].
+    - apply offered_prefix_here with
+        (k := fun _ : unit =>
+          schedule_with_offers_offer_prefix m n'
+            (fun i => embed (Fin.FS i)) v).
+      apply schedule_with_offers_offer_prefix_succ.
+    - apply offered_prefix_later with
+        (obs := ObsOffered (live_slot_ref (embed Fin.F1)))
+        (k := fun _ : unit =>
+          schedule_with_offers_offer_prefix m n'
+            (fun j => embed (Fin.FS j)) v).
+      + apply schedule_with_offers_offer_prefix_succ.
+      + apply (IH (fun j => embed (Fin.FS j))).
+  Qed.
+
+  Lemma offer_live_slot_now n (i : LiveSlot n)
+      (t : observed_completed E) :
+    <( {t}, {Obs (inl (ObsOffered (live_slot_ref i))) tt} |=
+         {offer_live_slot n i} )>.
+  Proof.
+    unfold offer_live_slot.
+    split; [reflexivity | constructor].
+  Qed.
+
+  Lemma observed_equ_refl_no_eqdep (t : observed_completed E) : t ≅ t.
+  Proof.
+    unfold equ.
+    apply (leq_gfp (@fequ _ _ unit unit eq)
+      (fun u v : observed_completed E => u = v)).
+    - intros u v <-. cbn. destruct (observe u); constructor; auto.
+    - reflexivity.
+  Qed.
+
+  Lemma observed_equ_step_no_eqdep (t u : observed_completed E) :
+    t ≅ u -> equF eq (equ eq) (observe t) (observe u).
+  Proof.
+    intro Htu. unfold equ in Htu.
+    exact (proj1 (gfp_fp (@fequ _ _ unit unit eq) t u) Htu).
+  Qed.
+
+  Definition equF_scheduler_vis_result
+      (p q : ictree' (scheduler_observedE E) unit) : Prop :=
+    match q with
+    | VisF (inl sched_obs) k_right =>
+        exists k_left,
+          p = VisF (inl sched_obs) k_left /\ k_left tt ≅ k_right tt
+    | _ => True
+    end.
+
+  Lemma equF_scheduler_vis_inv_no_eqdep p q :
+    equF eq (equ eq) p q -> equF_scheduler_vis_result p q.
+  Proof.
+    intro Hf.
+    destruct Hf as [x y Hxy | e k1 k2 Hk | t1 t2 Ht |
+        n k1 k2 Hk]; cbn; try exact I.
+    destruct e as [sched_obs | rest]; cbn; try exact I.
+    exists k1. split; [reflexivity | apply Hk].
+  Qed.
+
+  Lemma equ_scheduler_vis_inv_from_observe_no_eqdep
+      (obs : schedulerObsE)
+      (k : encode (inl obs : scheduler_observedE E) ->
+        observed_completed E)
+      (t u : observed_completed E) :
+    t ≅ u ->
+    observe u = VisF (inl obs) k ->
+    exists k_t, observe t = VisF (inl obs) k_t /\ k_t tt ≅ k tt.
+  Proof.
+    intros Htu Hu.
+    pose proof (equF_scheduler_vis_inv_no_eqdep _ _
+      (observed_equ_step_no_eqdep _ _ Htu)) as Hshape.
+    rewrite Hu in Hshape.
+    exact Hshape.
+  Qed.
+
+  Lemma ktrans_vis_raw_inv_no_eqdep {X} (e : scheduler_observedE E)
+      (k : encode e -> ictree (scheduler_observedE E) X)
+      (w : World (scheduler_observedE E)) t' w' :
+    |Vis e k, w| ↦ |t', w'| ->
+    exists v (target : ictree (scheduler_observedE E) X),
+      w' = Obs e v /\ observe target = observe t' /\
+      target ≅ k v /\ not_done w.
+  Proof.
+    intro Htr.
+    cbn in Htr.
+    refine (match Htr in ktrans_ ot w0 ot' w0' return
+        match ot with
+        | VisF e0 k0 =>
+            exists v (target : ictree (scheduler_observedE E) X),
+              w0' = Obs e0 v /\ observe target = ot' /\
+              target ≅ k0 v /\ not_done w0
+        | _ => True
+        end with
+      | KtransObs e0 v k0 target w0 Hnd Heq => _
+      | _ => I
+      end).
+    exists v, target.
+    split; [reflexivity | split; [reflexivity | split; assumption]].
+  Qed.
+
+  Lemma ktrans_scheduler_vis_inv_no_eqdep {X} (obs : schedulerObsE)
+      (k : encode (inl obs : scheduler_observedE E) ->
+        ictree (scheduler_observedE E) X)
+      (w : World (scheduler_observedE E)) t' w' :
+    |Vis (inl obs) k, w| ↦ |t', w'| ->
+    exists target : ictree (scheduler_observedE E) X,
+      w' = Obs (inl obs) tt /\ observe target = observe t' /\
+      target ≅ k tt /\ not_done w.
+  Proof.
+    intro Htr.
+    destruct (ktrans_vis_raw_inv_no_eqdep _ _ _ _ _ Htr) as
+      [v [target [Hw [Ht [Heq Hnd]]]]].
+    destruct v.
+    exists target. split; [exact Hw | split; [exact Ht | split; assumption]].
+  Qed.
+
+  Inductive SchedulerEquChain :
+      observed_completed E -> observed_completed E -> Prop :=
+  | scheduler_equ_chain_refl t : SchedulerEquChain t t
+  | scheduler_equ_chain_cons t u v :
+      t ≅ u ->
+      SchedulerEquChain u v ->
+      SchedulerEquChain t v.
+
+  Lemma scheduler_equ_chain_scheduler_vis_inv_no_eqdep
+      (obs : schedulerObsE)
+      (k : encode (inl obs : scheduler_observedE E) ->
+        observed_completed E)
+      (t u : observed_completed E) :
+    SchedulerEquChain t u ->
+    observe u = VisF (inl obs) k ->
+    exists k_t,
+      observe t = VisF (inl obs) k_t /\
+      SchedulerEquChain (k_t tt) (k tt).
+  Proof.
+    intros Hchain Hobs.
+    induction Hchain as [u | t mid u Htm _ IH].
+    - exists k. split; [exact Hobs | constructor].
+    - destruct (IH Hobs) as [k_mid [Hmid Hcont]].
+      destruct (equ_scheduler_vis_inv_from_observe_no_eqdep obs k_mid
+        t mid Htm Hmid) as [k_t [Ht Hstep]].
+      exists k_t. split; [exact Ht |].
+      econstructor; [exact Hstep | exact Hcont].
+  Qed.
+
+  Lemma offered_in_scheduler_prefix_chain_implies_AF n
+      (i : LiveSlot n) (u actual bridge : observed_completed E) w :
+    observe bridge = observe actual ->
+    SchedulerEquChain bridge u ->
+    not_done w ->
+    offered_in_scheduler_prefix n i u ->
+    <( {actual}, w |= AF {offer_live_slot n i} )>.
+  Proof.
+    intros Hbridge Hchain Hnd Hprefix.
+    revert actual bridge w Hbridge Hchain Hnd.
+    induction Hprefix as [u k Hobs | u obs k Hobs _ IH];
+      intros actual bridge w Hbridge Hchain Hnd.
+    - destruct (scheduler_equ_chain_scheduler_vis_inv_no_eqdep
+        (ObsOffered (live_slot_ref i)) k bridge u Hchain Hobs) as
+        [k_actual [Hactual Hcont]].
+      rewrite unfold_entailsL.
+      apply StepA.
+      split.
+      + split; [exact I | exact Hnd].
+      + split.
+        * exists (k_actual tt),
+            (Obs (inl (ObsOffered (live_slot_ref i))) tt).
+          cbn. rewrite <- Hbridge, Hactual.
+          constructor; [exact Hnd | apply observed_equ_refl_no_eqdep].
+        * intros t' w' Htr.
+          cbn in Htr.
+          rewrite <- Hbridge, Hactual in Htr.
+          destruct (ktrans_scheduler_vis_inv_no_eqdep
+            (ObsOffered (live_slot_ref i)) k_actual w t' w' Htr) as
+            [target [Hw' [Htarget [Heqtarget Hsource]]]].
+          subst w'.
+          apply MatchA.
+          unfold offer_live_slot.
+          split; [reflexivity | constructor].
+    - destruct (scheduler_equ_chain_scheduler_vis_inv_no_eqdep
+        obs k bridge u Hchain Hobs) as [k_actual [Hactual Hcont]].
+      rewrite unfold_entailsL.
+      apply StepA.
+      split.
+      + split; [exact I | exact Hnd].
+      + split.
+        * exists (k_actual tt), (Obs (inl obs) tt).
+          cbn. rewrite <- Hbridge, Hactual.
+          constructor; [exact Hnd | apply observed_equ_refl_no_eqdep].
+        * intros t' w' Htr.
+          cbn in Htr.
+          rewrite <- Hbridge, Hactual in Htr.
+          destruct (ktrans_scheduler_vis_inv_no_eqdep obs
+            k_actual w t' w' Htr) as
+            [target [Hw' [Htarget [Heqtarget Hsource]]]].
+          subst w'.
+          specialize (IH t' target (Obs (inl obs) tt) Htarget
+            (scheduler_equ_chain_cons target (k_actual tt) (k tt)
+              Heqtarget Hcont) (NotDoneObs (inl obs) tt)).
+          rewrite unfold_entailsL in IH.
+          exact IH.
+  Qed.
+
+  Theorem offered_in_scheduler_prefix_implies_AF n
+      (i : LiveSlot n) (t : observed_completed E) w :
+    not_done w ->
+    offered_in_scheduler_prefix n i t ->
+    <( {t}, w |= AF {offer_live_slot n i} )>.
+  Proof.
+    intros Hnd Hprefix.
+    eapply offered_in_scheduler_prefix_chain_implies_AF.
+    - reflexivity.
+    - constructor.
+    - exact Hnd.
+    - exact Hprefix.
+  Qed.
+
+  Lemma show_no_focus_offers_every_live_slot_prefix n
+      (v : pool E (S n)) (i : LiveSlot (S n)) :
+    offered_in_scheduler_prefix (S n) i
+      (schedule_with_offers (S n) v None).
+  Proof.
+    eapply offered_prefix_later.
+    - apply schedule_with_offers_no_focus_nonempty.
+    - apply (schedule_with_offers_offer_prefix_offers (S n) (S n)
+        (fun i => i) v i).
+  Qed.
+
+  Lemma no_focus_offers_every_live_slot_prefix n
+      (v : pool E (S n)) (i : LiveSlot (S n)) :
+    offered_in_scheduler_prefix (S n) i
+      (schedule_with_offers (S n) v None).
+  Proof.
+    apply show_no_focus_offers_every_live_slot_prefix.
+  Qed.
+
+  Theorem show_no_focus_offers_every_live_slot n
+      (v : pool E (S n)) (i : LiveSlot (S n)) :
+    <( {schedule_with_offers (S n) v None}, Pure |=
+         AF {offer_live_slot (S n) i} )>.
+  Proof.
+    apply offered_in_scheduler_prefix_implies_AF.
+    - constructor.
+    - apply show_no_focus_offers_every_live_slot_prefix.
+  Qed.
+
+  Theorem no_focus_offers_every_live_slot n
+      (v : pool E (S n)) (i : LiveSlot (S n)) :
+    <( {schedule_with_offers (S n) v None}, Pure |=
+         AF {offer_live_slot (S n) i} )>.
+  Proof.
+    apply show_no_focus_offers_every_live_slot.
+  Qed.
+
+  Definition scheduling_point_offer_obligation
+      (t : observed_completed E) (w : World (scheduler_observedE E))
+      : Prop :=
+    forall n,
+      w = Obs (inl (ObsSchedulingPoint (S n))) tt ->
+      forall i : LiveSlot (S n),
+        <( {t}, w |= AF {offer_live_slot (S n) i} )>.
+
+  Local Definition non_scheduling_point_world
+      (w : World (scheduler_observedE E)) : Prop :=
+    forall n,
+      w = Obs (inl (ObsSchedulingPoint (S n))) tt -> False.
+
+  Local Lemma pure_non_scheduling_point :
+    non_scheduling_point_world Pure.
+  Proof. intros n Hcontra. discriminate Hcontra. Qed.
+
+  Local Lemma obs_offered_non_scheduling_point ref :
+    non_scheduling_point_world
+      (Obs (inl (ObsOffered ref) : scheduler_observedE E) tt).
+  Proof. intros n Hcontra. discriminate Hcontra. Qed.
+
+  Local Lemma obs_non_scheduler_non_scheduling_point
+      (event : yieldE + (spawnE + E))
+      (value : encode (inr event : scheduler_observedE E)) :
+    non_scheduling_point_world (Obs (inr event) value).
+  Proof. intros n Hcontra. discriminate Hcontra. Qed.
+
+  Private Inductive SchedulerOfferCanonical
+      : observed_completed E -> World (scheduler_observedE E) -> Prop :=
+  | scheduler_offer_canonical_schedule : forall n
+      (v : pool E n) focus w,
+      non_scheduling_point_world w ->
+      SchedulerOfferCanonical (schedule_with_offers n v focus) w
+  | scheduler_offer_canonical_prefix_at_point : forall n
+      (v : pool E (S n)),
+      SchedulerOfferCanonical
+        (schedule_with_offers_offer_prefix (S n) (S n)
+          (fun i : LiveSlot (S n) => i) v)
+        (Obs (inl (ObsSchedulingPoint (S n))) tt)
+  | scheduler_offer_canonical_prefix_elsewhere : forall m r
+      (embed : LiveSlot r -> LiveSlot m) (v : pool E m) w,
+      non_scheduling_point_world w ->
+      SchedulerOfferCanonical
+        (schedule_with_offers_offer_prefix m r embed v) w
+  | scheduler_offer_canonical_choice : forall n
+      (v : pool E (S n)) w,
+      non_scheduling_point_world w ->
+      SchedulerOfferCanonical
+        (Br n (fun i : fin' n =>
+          schedule_with_offers (S n) v (Some i))) w
+  | scheduler_offer_canonical_done : forall t (x : unit),
+      SchedulerOfferCanonical t (Done x)
+  | scheduler_offer_canonical_finish : forall t
+      (event : scheduler_observedE E) (value : encode event) (x : unit),
+      SchedulerOfferCanonical t (Finish event value x).
+
+  Local Definition SchedulerOfferShape
+      (t : observed_completed E) (w : World (scheduler_observedE E))
+      : Prop :=
+    exists u : observed_completed E, t ≅ u /\ SchedulerOfferCanonical u w.
+
+  Local Lemma scheduler_offer_shape_canonical t w :
+    SchedulerOfferCanonical t w -> SchedulerOfferShape t w.
+  Proof.
+    intro Hcanonical.
+    exists t. split; [apply observed_equ_refl_no_eqdep | exact Hcanonical].
+  Qed.
+
+  Local Lemma scheduler_offer_shape_equ t u w :
+    t ≅ u -> SchedulerOfferShape u w -> SchedulerOfferShape t w.
+  Proof.
+    intros Htu [v [Huv Hcanonical]].
+    exists v. split.
+    - transitivity u; assumption.
+    - exact Hcanonical.
+  Qed.
+
+  Local Lemma observed_equ_of_observe_eq (t u : observed_completed E) :
+    observe t = observe u -> t ≅ u.
+  Proof.
+    intro Hobserve.
+    transitivity (go (observe t)).
+    - apply ictree_eta.
+    - rewrite Hobserve.
+      symmetry. apply ictree_eta.
+  Qed.
+
+  Local Lemma scheduler_offer_shape_schedule n
+      (v : pool E n) focus w :
+    non_scheduling_point_world w ->
+    SchedulerOfferShape (schedule_with_offers n v focus) w.
+  Proof.
+    intro Hworld.
+    apply scheduler_offer_shape_canonical.
+    now constructor.
+  Qed.
+
+  Local Lemma scheduler_offer_shape_prefix_at_point n
+      (v : pool E (S n)) :
+    SchedulerOfferShape
+      (schedule_with_offers_offer_prefix (S n) (S n)
+        (fun i : LiveSlot (S n) => i) v)
+      (Obs (inl (ObsSchedulingPoint (S n))) tt).
+  Proof.
+    apply scheduler_offer_shape_canonical.
+    constructor.
+  Qed.
+
+  Local Lemma scheduler_offer_shape_prefix_elsewhere m r
+      (embed : LiveSlot r -> LiveSlot m) (v : pool E m) w :
+    non_scheduling_point_world w ->
+    SchedulerOfferShape
+      (schedule_with_offers_offer_prefix m r embed v) w.
+  Proof.
+    intro Hworld.
+    apply scheduler_offer_shape_canonical.
+    now constructor.
+  Qed.
+
+  Local Lemma scheduler_offer_shape_choice n
+      (v : pool E (S n)) w :
+    non_scheduling_point_world w ->
+    SchedulerOfferShape
+      (Br n (fun i : fin' n =>
+        schedule_with_offers (S n) v (Some i))) w.
+  Proof.
+    intro Hworld.
+    apply scheduler_offer_shape_canonical.
+    now constructor.
+  Qed.
+
+  Local Lemma scheduler_offer_shape_done t (x : unit) :
+    SchedulerOfferShape t (Done x).
+  Proof.
+    apply scheduler_offer_shape_canonical.
+    constructor.
+  Qed.
+
+  Local Lemma scheduler_offer_shape_finish t
+      (event : scheduler_observedE E) (value : encode event) (x : unit) :
+    SchedulerOfferShape t (Finish event value x).
+  Proof.
+    apply scheduler_offer_shape_canonical.
+    constructor.
+  Qed.
+
+  Local Lemma scheduler_offer_canonical_obligation t w :
+    SchedulerOfferCanonical t w -> scheduling_point_offer_obligation t w.
+  Proof.
+    intro Hcanonical.
+    destruct Hcanonical as
+      [n v focus w Hworld | n v | m r embed v w Hworld |
+       n v w Hworld | t x | t event value x].
+    - intros k Hsched i.
+      exfalso. exact (Hworld k Hsched).
+    - intros k Hsched i.
+      inversion Hsched; subst.
+      apply offered_in_scheduler_prefix_implies_AF.
+      + constructor.
+      + apply (schedule_with_offers_offer_prefix_offers (S k) (S k)
+          (fun j : LiveSlot (S k) => j) v i).
+    - intros k Hsched i.
+      exfalso. exact (Hworld k Hsched).
+    - intros k Hsched i.
+      exfalso. exact (Hworld k Hsched).
+    - intros k Hsched i. discriminate Hsched.
+    - intros k Hsched i. discriminate Hsched.
+  Qed.
+
+  Local Lemma scheduler_offer_shape_obligation t w :
+    SchedulerOfferShape t w -> scheduling_point_offer_obligation t w.
+  Proof.
+    intros [u [Htu Hcanonical]] k Hsched i.
+    rewrite Htu.
+    eapply scheduler_offer_canonical_obligation; eauto.
+  Qed.
+
+  Local Lemma scheduler_offer_shape_ret_step
+      (w : World (scheduler_observedE E)) t' w' :
+    |Ret tt, w| ↦ |t', w'| -> SchedulerOfferShape t' w'.
+  Proof.
+    intro Htr.
+    destruct w as [| event value | x | event value x].
+    - apply ktrans_done in Htr as [-> _].
+      apply scheduler_offer_shape_done.
+    - apply ktrans_finish in Htr as [-> _].
+      apply scheduler_offer_shape_finish.
+    - apply ktrans_not_done in Htr. inversion Htr.
+    - apply ktrans_not_done in Htr. inversion Htr.
+  Qed.
+
+  Local Lemma scheduler_offer_canonical_step t w t' w' :
+    SchedulerOfferCanonical t w ->
+    |t, w| ↦ |t', w'| ->
+    SchedulerOfferShape t' w'.
+  Proof.
+    intros Hcanonical Htr.
+    revert t w t' w' Hcanonical Htr.
+    fix IH 6.
+    intros t w t' w' Hcanonical Htr.
+    destruct Hcanonical as
+      [n v focus w Hworld | n v | m r embed v w Hworld |
+       n v w Hworld | t x | t event value x].
+    - destruct focus as [slot |].
+      + dependent destruction slot.
+        * set (focused_slot := (Fin.F1 : Fin.t (S n))).
+          destruct (observe (v focused_slot)) eqn:Hthread;
+          fold focused_slot in Htr.
+          -- destruct x.
+             cbn in Htr.
+             rewrite (schedule_with_offers_focused_ret
+               n v focused_slot Hthread) in Htr.
+             dependent destruction Htr.
+             eapply scheduler_offer_shape_equ.
+             ++ apply observed_equ_of_observe_eq.
+                match goal with
+                | Hobs : observe ?mid = observe t' |- _ =>
+                    symmetry; exact Hobs
+                end.
+             ++ eapply IH.
+                ** apply scheduler_offer_canonical_schedule.
+                   exact Hworld.
+                ** exact Htr.
+          -- cbn in Htr.
+             rewrite (schedule_with_offers_focused_br
+               n v focused_slot n0 k Hthread) in Htr.
+             apply ktrans_br in Htr as [choice [Htarget [-> _]]].
+             eapply scheduler_offer_shape_equ.
+             ++ exact Htarget.
+             ++ apply scheduler_offer_shape_schedule. exact Hworld.
+          -- cbn in Htr.
+             rewrite (schedule_with_offers_focused_guard
+               n v focused_slot t Hthread) in Htr.
+             dependent destruction Htr.
+             eapply scheduler_offer_shape_equ.
+             ++ apply observed_equ_of_observe_eq.
+                match goal with
+                | Hobs : observe ?mid = observe t' |- _ =>
+                    symmetry; exact Hobs
+                end.
+             ++ eapply IH.
+                ** apply scheduler_offer_canonical_schedule.
+                   exact Hworld.
+                ** exact Htr.
+          -- destruct e as [yield_event | [spawn_event | user_event]].
+             ++ destruct yield_event.
+                cbn in Htr.
+                rewrite (schedule_with_offers_focused_yield
+                  n v focused_slot k Hthread) in Htr.
+                dependent destruction Htr.
+                eapply scheduler_offer_shape_equ.
+                ** apply observed_equ_of_observe_eq.
+                   match goal with
+                   | Hobs : observe ?mid = observe t' |- _ =>
+                       symmetry; exact Hobs
+                   end.
+                ** eapply IH.
+                   --- apply scheduler_offer_canonical_schedule.
+                       exact Hworld.
+                   --- exact Htr.
+             ++ destruct spawn_event.
+                cbn in Htr.
+                rewrite (schedule_with_offers_focused_fork
+                  n v focused_slot k Hthread) in Htr.
+                apply ktrans_vis in Htr as [[] [-> [Htarget _]]].
+                eapply scheduler_offer_shape_equ.
+                ** symmetry. exact Htarget.
+                ** apply scheduler_offer_shape_schedule.
+                   apply obs_non_scheduler_non_scheduling_point.
+             ++ cbn in Htr.
+                rewrite (schedule_with_offers_focused_user_event
+                  n v focused_slot user_event k Hthread) in Htr.
+                apply ktrans_vis in Htr as [value [-> [Htarget _]]].
+                eapply scheduler_offer_shape_equ.
+                ** symmetry. exact Htarget.
+                ** apply scheduler_offer_shape_schedule.
+                   apply obs_non_scheduler_non_scheduling_point.
+        * set (focused_slot := Fin.FS slot).
+          destruct (observe (v focused_slot)) eqn:Hthread;
+          fold focused_slot in Htr.
+          -- destruct x.
+             cbn in Htr.
+             rewrite (schedule_with_offers_focused_ret
+               n v focused_slot Hthread) in Htr.
+             dependent destruction Htr.
+             eapply scheduler_offer_shape_equ.
+             ++ apply observed_equ_of_observe_eq.
+                match goal with
+                | Hobs : observe ?mid = observe t' |- _ =>
+                    symmetry; exact Hobs
+                end.
+             ++ eapply IH.
+                ** apply scheduler_offer_canonical_schedule.
+                   exact Hworld.
+                ** exact Htr.
+          -- cbn in Htr.
+             rewrite (schedule_with_offers_focused_br
+               n v focused_slot n0 k Hthread) in Htr.
+             apply ktrans_br in Htr as [choice [Htarget [-> _]]].
+             eapply scheduler_offer_shape_equ.
+             ++ exact Htarget.
+             ++ apply scheduler_offer_shape_schedule. exact Hworld.
+          -- cbn in Htr.
+             rewrite (schedule_with_offers_focused_guard
+               n v focused_slot t Hthread) in Htr.
+             dependent destruction Htr.
+             eapply scheduler_offer_shape_equ.
+             ++ apply observed_equ_of_observe_eq.
+                match goal with
+                | Hobs : observe ?mid = observe t' |- _ =>
+                    symmetry; exact Hobs
+                end.
+             ++ eapply IH.
+                ** apply scheduler_offer_canonical_schedule.
+                   exact Hworld.
+                ** exact Htr.
+          -- destruct e as [yield_event | [spawn_event | user_event]].
+             ++ destruct yield_event.
+                cbn in Htr.
+                rewrite (schedule_with_offers_focused_yield
+                  n v focused_slot k Hthread) in Htr.
+                dependent destruction Htr.
+                eapply scheduler_offer_shape_equ.
+                ** apply observed_equ_of_observe_eq.
+                   match goal with
+                   | Hobs : observe ?mid = observe t' |- _ =>
+                       symmetry; exact Hobs
+                   end.
+                ** eapply IH.
+                   --- apply scheduler_offer_canonical_schedule.
+                       exact Hworld.
+                   --- exact Htr.
+             ++ destruct spawn_event.
+                cbn in Htr.
+                rewrite (schedule_with_offers_focused_fork
+                  n v focused_slot k Hthread) in Htr.
+                apply ktrans_vis in Htr as [[] [-> [Htarget _]]].
+                eapply scheduler_offer_shape_equ.
+                ** symmetry. exact Htarget.
+                ** apply scheduler_offer_shape_schedule.
+                   apply obs_non_scheduler_non_scheduling_point.
+             ++ cbn in Htr.
+                rewrite (schedule_with_offers_focused_user_event
+                  n v focused_slot user_event k Hthread) in Htr.
+                apply ktrans_vis in Htr as [value [-> [Htarget _]]].
+                eapply scheduler_offer_shape_equ.
+                ** symmetry. exact Htarget.
+                ** apply scheduler_offer_shape_schedule.
+                   apply obs_non_scheduler_non_scheduling_point.
+      + destruct n as [| n'].
+        * cbn in Htr.
+          apply scheduler_offer_shape_ret_step with (w := w).
+          exact Htr.
+        * cbn in Htr.
+          apply ktrans_vis in Htr as [[] [-> [Htarget _]]].
+          eapply scheduler_offer_shape_equ.
+          -- symmetry. exact Htarget.
+          -- apply scheduler_offer_shape_prefix_at_point.
+    - cbn in Htr.
+      apply ktrans_vis in Htr as [[] [-> [Htarget _]]].
+      eapply scheduler_offer_shape_equ.
+      + symmetry. exact Htarget.
+      + apply scheduler_offer_shape_prefix_elsewhere.
+        apply obs_offered_non_scheduling_point.
+    - destruct r as [| r'].
+      + destruct m as [| m'].
+        * cbn in Htr.
+          apply scheduler_offer_shape_ret_step with (w := w).
+          exact Htr.
+        * cbn in Htr.
+          apply ktrans_vis in Htr as [[] [-> [Htarget _]]].
+          eapply scheduler_offer_shape_equ.
+          -- symmetry. exact Htarget.
+          -- apply scheduler_offer_shape_choice.
+             apply obs_non_scheduler_non_scheduling_point.
+      + cbn in Htr.
+        apply ktrans_vis in Htr as [[] [-> [Htarget _]]].
+        eapply scheduler_offer_shape_equ.
+        * symmetry. exact Htarget.
+        * apply scheduler_offer_shape_prefix_elsewhere.
+          apply obs_offered_non_scheduling_point.
+    - cbn in Htr.
+      apply ktrans_br in Htr as [choice [Htarget [-> _]]].
+      eapply scheduler_offer_shape_equ.
+      + exact Htarget.
+      + apply scheduler_offer_shape_schedule. exact Hworld.
+    - apply ktrans_not_done in Htr. inversion Htr.
+    - apply ktrans_not_done in Htr. inversion Htr.
+  Qed.
+
+  Local Lemma scheduler_offer_shape_step t w t' w' :
+    SchedulerOfferShape t w ->
+    |t, w| ↦ |t', w'| ->
+    SchedulerOfferShape t' w'.
+  Proof.
+    intros [u [Htu Hcanonical]] Htr.
+    rewrite Htu in Htr.
+    eapply scheduler_offer_canonical_step; eauto.
+  Qed.
+
+  CoInductive SchedulerProgress
+      : observed_completed E -> World (scheduler_observedE E) -> Prop :=
+  | scheduler_progress_intro : forall t w,
+      can_step t w ->
+      (forall t' w',
+        |t, w| ↦ |t', w'| -> SchedulerProgress t' w') ->
+      SchedulerProgress t w.
+
+  Lemma scheduler_progress_shape_implies_AG t w :
+    SchedulerProgress t w ->
+    SchedulerOfferShape t w ->
+    agc scheduling_point_offer_obligation t w.
+  Proof.
+    intros Hprogress0 Hshape0.
+    pose proof (leq_gfp (agcF scheduling_point_offer_obligation)
+      (fun t w => SchedulerProgress t w /\ SchedulerOfferShape t w))
+      as Hcoind.
+    apply Hcoind.
+    - clear t w Hprogress0 Hshape0.
+      intros t w [Hprogress Hshape].
+      destruct Hprogress as [t w Hstep Hnext].
+      split.
+      + apply scheduler_offer_shape_obligation. exact Hshape.
+      + split.
+        * exact Hstep.
+        * intros t' w' Htr.
+          split.
+          -- apply Hnext. exact Htr.
+          -- eapply scheduler_offer_shape_step; eauto.
+    - split; assumption.
+  Qed.
+
+  Theorem every_live_slot_is_eventually_offered_at_scheduling_points
+      n (v : pool E n) focus :
+    SchedulerProgress (schedule_with_offers n v focus) Pure ->
+    agc scheduling_point_offer_obligation
+      (schedule_with_offers n v focus) Pure.
+  Proof.
+    intro Hprogress.
+    eapply scheduler_progress_shape_implies_AG.
+    - exact Hprogress.
+    - apply scheduler_offer_shape_schedule.
+      apply pure_non_scheduling_point.
+  Qed.
+
+  Theorem show_every_live_slot_is_eventually_offered_at_scheduling_points
+      n (v : pool E n) focus :
+    SchedulerProgress (schedule_with_offers n v focus) Pure ->
+    agc scheduling_point_offer_obligation
+      (schedule_with_offers n v focus) Pure.
+  Proof.
+    apply every_live_slot_is_eventually_offered_at_scheduling_points.
+  Qed.
+End ObservedScheduler.
diff --git a/theories/Lang/Yield/Syntax.v b/theories/Lang/Yield/Syntax.v
new file mode 100644
index 0000000..5c6a554
--- /dev/null
+++ b/theories/Lang/Yield/Syntax.v
@@ -0,0 +1,29 @@
+From Stdlib Require Import Nat Strings.String.
+
+Module YieldSyntax.
+  Definition var := string.
+  Definition value := nat.
+
+  Inductive YExp : Type :=
+  | YVar (_ : var)
+  | YLit (_ : value)
+  | YPlus (_ _ : YExp)
+  | YMinus (_ _ : YExp)
+  | YMult (_ _ : YExp).
+
+  Inductive YStmt : Type :=
+  | YAssign (x : var) (e : YExp)
+  | YSeq (a b : YStmt)
+  | YIf (i : YExp) (t e : YStmt)
+  | YWhile (t : YExp) (b : YStmt)
+  (** [YFork body] spawns [body] as the child-side statement.
+      The parent path performs no source statement at the fork node; it
+      continues through the surrounding sequence. *)
+  | YFork (body : YStmt)
+  | YSkip
+  | YYield.
+
+  (** Yield treats any non-zero natural as true. *)
+  Definition is_true (v : value) : bool := negb (v =? 0).
+End YieldSyntax.
+Export YieldSyntax.
diff --git a/theories/Lang/Yield/Ticl.v b/theories/Lang/Yield/Ticl.v
new file mode 100644
index 0000000..477e819
--- /dev/null
+++ b/theories/Lang/Yield/Ticl.v
@@ -0,0 +1,1347 @@
+(** TICL-facing Yield surface.
+
+    Public tiers exported by this façade:
+
+    - [Lang.Yield.Events], [Lang.Yield.Syntax], and [Lang.Yield.Denote] expose
+      raw source-level threads with [Yield], [Fork], and memory effects.
+    - [Lang.Yield.Scheduler] exposes the scheduler, and [scheduled_visible]
+      exposes scheduled programs with scheduler [Spawn], cooperative [Yield],
+      and memory effects visible.
+    - [interp_scheduled_erased], [instr_exp_erased], and [instr_stmt_erased]
+      expose the state-only TICL view where scheduler/yield observations are
+      intentionally erased.
+    - [interp_scheduled], [instr_exp], and [instr_stmt] are compatibility
+      aliases for the erased tier.
+
+    This file also carries a small regression surface: constructor unfold facts,
+    one-step scheduler facts, finite-pool slot regressions, concrete visible
+    YYield/YFork examples, and alias facts documenting that the compatibility
+    APIs are erased. *)
+From Stdlib Require Import
+  Fin
+  Morphisms
+  Nat
+  Program.Equality
+  Strings.String.
+
+From ExtLib Require Import
+  Data.Map.FMapAList
+  Data.String
+  Structures.Maps.
+
+From TICL Require Export
+  Lang.Yield.Events
+  Lang.Yield.Syntax
+  Lang.Yield.Denote
+  Lang.Yield.Vec
+  Lang.Yield.Scheduler
+  Lang.Yield.Interp.
+
+From TICL Require Import
+  ICTree.Core
+  ICTree.Equ
+  ICTree.Eq.Bind
+  ICTree.Events.Writer
+  ICTree.Interp.Core
+  ICTree.Interp.State
+  ICTree.Logic.AX
+  ICTree.Logic.AF
+  ICTree.Logic.Bind
+  ICTree.Logic.CanStep
+  ICTree.Logic.Iter
+  ICTree.Logic.State
+  ICTree.SBisim
+  Logic.Core.
+
+Import ICtree ICTreeNotations TiclNotations.
+Local Open Scope ticl_scope.
+Local Open Scope ictree_scope.
+
+Local Typeclasses Transparent equ.
+Lemma interp_equ_hetero
+    {E F : Type} `{Encode E} `{Encode F} {X}
+    (h : E ~> ictree F) :
+  forall (x y : ictree E X),
+    x ≅ y -> @equ F _ X X eq (interp h x) (interp h y).
+Proof.
+  change (forall x y : ictree E X,
+             @equ E _ X X eq x y ->
+             @equ F _ X X eq (interp h x) (interp h y)).
+  __coinduction_equ RR IH; intros * EQ1.
+  setoid_rewrite unfold_iter.
+  step in EQ1; inv EQ1.
+  - setoid_rewrite bind_ret_l; reflexivity.
+  - setoid_rewrite bind_bind; setoid_rewrite bind_ret_l.
+    upto_bind_equ.
+    constructor. intros.
+    apply IH. apply H3.
+  - setoid_rewrite bind_ret_l.
+    constructor.
+    apply IH. apply H3.
+  - setoid_rewrite bind_bind.
+    upto_bind_equ.
+    setoid_rewrite bind_ret_l.
+    constructor.
+    apply IH. apply H3.
+Qed.
+
+#[local] Instance interp_equ_hetero_proper
+    {E F : Type} `{Encode E} `{Encode F} {X}
+    (h : E ~> ictree F) :
+  Proper (equ eq ==> equ eq) (@interp E _ _ _ _ _ h X).
+Proof.
+  intros x y Hxy.
+  now apply interp_equ_hetero.
+Qed.
+
+Lemma interp_bind_hetero
+    {E F : Type} `{Encode E} `{Encode F} {A B}
+    (h : E ~> ictree F) (t : ictree E A) (k : A -> ictree E B) :
+  interp h (x <- t;; k x) ≅ (x <- interp h t;; interp h (k x)).
+Proof.
+  revert t.
+  __coinduction_equ RR IH; intros.
+  rewrite (ictree_eta t).
+  rewrite unfold_bind, unfold_interp.
+  destruct (observe t) eqn:Hobs; cbn.
+  - rewrite unfold_interp.
+    cbn.
+    rewrite bind_ret_l.
+    rewrite unfold_interp.
+    reflexivity.
+  - rewrite unfold_interp.
+    cbn.
+    rewrite bind_br.
+    setoid_rewrite bind_guard.
+    constructor; intro i.
+    step; econstructor; intros.
+    apply IH.
+  - rewrite (@unfold_interp _ _ _ _ _ h (Guard t0)).
+    cbn.
+    rewrite bind_guard.
+    constructor.
+    apply IH.
+  - rewrite unfold_interp.
+    cbn.
+    rewrite bind_bind.
+    upto_bind_equ.
+    rewrite bind_guard.
+    constructor.
+    apply IH.
+Qed.
+
+(** Expression denotation constructor unfold facts. *)
+Lemma denote_exp_yvar name :
+  denote_exp (YVar name) =
+    (ctx <- yget;;
+     match lookup name ctx with
+     | Some value => yyield;; Ret value
+     | None => stuck
+     end).
+Proof. reflexivity. Qed.
+
+Lemma denote_exp_ylit n : denote_exp (YLit n) = Ret n.
+Proof. reflexivity. Qed.
+
+Lemma denote_exp_yplus a b :
+  denote_exp (YPlus a b) =
+    (x <- denote_exp a;; y <- denote_exp b;; Ret (x + y)%nat).
+Proof. reflexivity. Qed.
+
+Lemma denote_exp_yminus a b :
+  denote_exp (YMinus a b) =
+    (x <- denote_exp a;; y <- denote_exp b;; Ret (x - y)%nat).
+Proof. reflexivity. Qed.
+
+Lemma denote_exp_ymult a b :
+  denote_exp (YMult a b) =
+    (x <- denote_exp a;; y <- denote_exp b;; Ret (x * y)%nat).
+Proof. reflexivity. Qed.
+
+(** Flow-sensitive statement denotation constructor unfold facts. *)
+Lemma denote_stmt_unfold s :
+  denote_stmt s = (_ <- denote_stmt_flow s;; Ret tt).
+Proof. reflexivity. Qed.
+
+Lemma denote_stmt_flow_yassign name expr :
+  denote_stmt_flow (YAssign name expr) =
+    (value <- denote_exp expr;;
+     ctx <- yget;;
+     yput (add name value ctx);;
+     Ret Fallthrough).
+Proof. reflexivity. Qed.
+
+Lemma denote_stmt_flow_yseq a b :
+  denote_stmt_flow (YSeq a b) =
+    (flow <- denote_stmt_flow a;;
+     match flow with
+     | Fallthrough => denote_stmt_flow b
+     | HaltThread => Ret HaltThread
+     end).
+Proof. reflexivity. Qed.
+
+Lemma denote_stmt_flow_yif test then_branch else_branch :
+  denote_stmt_flow (YIf test then_branch else_branch) =
+    (condition_value <- denote_exp test;;
+     if YieldSyntax.is_true condition_value then
+       denote_stmt_flow then_branch
+     else
+       denote_stmt_flow else_branch).
+Proof. reflexivity. Qed.
+
+Lemma denote_stmt_flow_ywhile test body :
+  denote_stmt_flow (YWhile test body) =
+    ICtree.iter
+      (fun _ =>
+         condition_value <- denote_exp test;;
+         if YieldSyntax.is_true condition_value then
+           flow <- denote_stmt_flow body;;
+           match flow with
+           | Fallthrough => Ret (inl tt)
+           | HaltThread => Ret (inr HaltThread)
+           end
+         else
+           Ret (inr Fallthrough)) tt.
+Proof. reflexivity. Qed.
+
+Lemma denote_stmt_flow_yfork body :
+  denote_stmt_flow (YFork body) =
+    (in_child <- yfork;;
+     if in_child then
+       _ <- denote_stmt_flow body;;
+       Ret HaltThread
+     else
+       Ret Fallthrough).
+Proof. reflexivity. Qed.
+
+Lemma denote_stmt_yfork body :
+  denote_stmt (YFork body) =
+    (_ <- (in_child <- yfork;;
+           if in_child then
+             _ <- denote_stmt_flow body;;
+             Ret HaltThread
+           else
+             Ret Fallthrough);;
+     Ret tt).
+Proof. reflexivity. Qed.
+
+Lemma denote_stmt_flow_yskip : denote_stmt_flow YSkip = Ret Fallthrough.
+Proof. reflexivity. Qed.
+
+Lemma denote_stmt_flow_yyield :
+  denote_stmt_flow YYield = (yyield;; Ret Fallthrough).
+Proof. reflexivity. Qed.
+
+(** Erased source-structural facts for the state-only TICL tier. *)
+Local Ltac unfold_erased_expression :=
+  unfold instr_exp_erased, interp_thread, interp_yield, instr_stateE;
+  cbn;
+  setoid_rewrite unfold_interp;
+  cbn.
+
+Local Ltac unfold_erased_statement :=
+  unfold instr_stmt_erased, interp_scheduled_erased, interp_yield,
+    interp_spawn, scheduled_visible, instr_stateE;
+  cbn;
+  setoid_rewrite unfold_interp;
+  cbn.
+
+Local Ltac step_erased_state :=
+  rewrite interp_state_tau, sb_guard;
+  setoid_rewrite unfold_interp;
+  cbn.
+
+Local Ltac expose_erased_get_result ctx :=
+  rewrite interp_state_tau, sb_guard;
+  change (resum_ret (inr (inr StateE.Get)) (resum_ret StateE.Get ctx))
+    with ctx;
+  setoid_rewrite unfold_interp;
+  cbn;
+  rewrite interp_state_tau, sb_guard;
+  setoid_rewrite unfold_interp;
+  cbn.
+
+Local Ltac step_erased_state3 :=
+  step_erased_state; step_erased_state; step_erased_state.
+
+(** Flow-preserving erased statement instrumentation for structural facts whose
+    contracts must expose [Fallthrough] versus [HaltThread].  The public
+    [instr_stmt_erased] remains the scheduled unit-returning view. *)
+Definition instr_stmt_flow_erased
+    (s : YStmt) (ctx : Ctx) : ictreeW Ctx (YStmtFlow * Ctx) :=
+  instr_stateE (interp_thread (denote_stmt_flow s)) ctx.
+
+Lemma axr_yexp_ylit : forall n n' ctx ctx' w w',
+    n = n' ->
+    ctx = ctx' ->
+    w = w' ->
+    not_done w ->
+    <[ {instr_exp_erased (YLit n) ctx},
+       w |= AX done= {(n', ctx')} w' ]>.
+Proof.
+  intros; subst.
+  unfold_erased_expression.
+  rewrite interp_state_ret.
+  now apply axr_ret.
+Qed.
+
+Lemma axr_yexp_yvar_some : forall name value ctx ctx' w w',
+    lookup name ctx = Some value ->
+    ctx = ctx' ->
+    w = w' ->
+    not_done w ->
+    <[ {instr_exp_erased (YVar name) ctx},
+       w |= AX done= {(value, ctx')} w' ]>.
+Proof.
+  intros; subst.
+  unfold_erased_expression.
+  eapply anr_state_bind_r_eq.
+  - rewrite interp_state_get.
+    now apply axr_ret.
+  - cbn.
+    rewrite interp_state_tau, sb_guard.
+    change (resum_ret (inr (inr StateE.Get)) (resum_ret StateE.Get ctx'))
+      with ctx'.
+    setoid_rewrite subst_ret_l.
+    cbn.
+    setoid_rewrite unfold_interp.
+    cbn.
+    rewrite interp_state_tau, sb_guard.
+    setoid_rewrite subst_ret_l.
+    cbn.
+    setoid_rewrite unfold_interp.
+    cbn.
+    change (alist_find RelDec_string name ctx') with (lookup name ctx').
+    destruct (lookup name ctx') eqn:Hlookup; try congruence.
+    inv H.
+    cbn.
+    rewrite bind_ret_l.
+    repeat (rewrite interp_state_tau, sb_guard).
+    change (resum_ret (inl Yield) (resum_ret Yield tt)) with tt.
+    rewrite subst_ret_l.
+    cbn.
+    setoid_rewrite unfold_interp.
+    cbn.
+    rewrite interp_state_tau, sb_guard.
+    rewrite subst_ret_l.
+    cbn.
+    setoid_rewrite unfold_interp.
+    cbn.
+    rewrite interp_state_ret.
+    now apply axr_ret.
+Qed.
+
+Lemma axr_yexp_yplus : forall a b x y value ctx ctx' w w',
+    <[ {instr_exp_erased a ctx}, w |= AX done= {(x, ctx)} w ]> ->
+    <[ {instr_exp_erased b ctx}, w |= AX done= {(y, ctx)} w ]> ->
+    value = (x + y)%nat ->
+    ctx = ctx' ->
+    w = w' ->
+    not_done w ->
+    <[ {instr_exp_erased (YPlus a b) ctx},
+       w |= AX done= {(value, ctx')} w' ]>.
+Proof.
+  intros a b x y value ctx ctx' w w' Ha Hb Hvalue Hctx Hw Hnd.
+  subst.
+  unfold instr_exp_erased, interp_thread, interp_yield, instr_stateE in *.
+  cbn.
+  rewrite !interp_bind_hetero.
+  rewrite !interp_state_bind.
+  eapply anr_bind_r_eq.
+  - exact Ha.
+  - cbn.
+    rewrite !interp_bind_hetero.
+    rewrite !interp_state_bind.
+    eapply anr_bind_r_eq.
+    + exact Hb.
+    + cbn.
+      rewrite !unfold_interp.
+      cbn.
+      rewrite interp_state_ret.
+      apply axr_ret; auto.
+Qed.
+
+Lemma axr_yexp_yminus : forall a b x y value ctx ctx' w w',
+    <[ {instr_exp_erased a ctx}, w |= AX done= {(x, ctx)} w ]> ->
+    <[ {instr_exp_erased b ctx}, w |= AX done= {(y, ctx)} w ]> ->
+    value = (x - y)%nat ->
+    ctx = ctx' ->
+    w = w' ->
+    not_done w ->
+    <[ {instr_exp_erased (YMinus a b) ctx},
+       w |= AX done= {(value, ctx')} w' ]>.
+Proof.
+  intros a b x y value ctx ctx' w w' Ha Hb Hvalue Hctx Hw Hnd.
+  subst.
+  unfold instr_exp_erased, interp_thread, interp_yield, instr_stateE in *.
+  cbn.
+  rewrite !interp_bind_hetero.
+  rewrite !interp_state_bind.
+  eapply anr_bind_r_eq.
+  - exact Ha.
+  - cbn.
+    rewrite !interp_bind_hetero.
+    rewrite !interp_state_bind.
+    eapply anr_bind_r_eq.
+    + exact Hb.
+    + cbn.
+      rewrite !unfold_interp.
+      cbn.
+      rewrite interp_state_ret.
+      apply axr_ret; auto.
+Qed.
+
+Lemma axr_yexp_ymult : forall a b x y value ctx ctx' w w',
+    <[ {instr_exp_erased a ctx}, w |= AX done= {(x, ctx)} w ]> ->
+    <[ {instr_exp_erased b ctx}, w |= AX done= {(y, ctx)} w ]> ->
+    value = (x * y)%nat ->
+    ctx = ctx' ->
+    w = w' ->
+    not_done w ->
+    <[ {instr_exp_erased (YMult a b) ctx},
+       w |= AX done= {(value, ctx')} w' ]>.
+Proof.
+  intros a b x y value ctx ctx' w w' Ha Hb Hvalue Hctx Hw Hnd.
+  subst.
+  unfold instr_exp_erased, interp_thread, interp_yield, instr_stateE in *.
+  cbn.
+  rewrite !interp_bind_hetero.
+  rewrite !interp_state_bind.
+  eapply anr_bind_r_eq.
+  - exact Ha.
+  - cbn.
+    rewrite !interp_bind_hetero.
+    rewrite !interp_state_bind.
+    eapply anr_bind_r_eq.
+    + exact Hb.
+    + cbn.
+      rewrite !unfold_interp.
+      cbn.
+      rewrite interp_state_ret.
+      apply axr_ret; auto.
+Qed.
+
+Lemma axr_yexp_yplus_ylit_ylit : forall x y value ctx ctx' w w',
+    value = (x + y)%nat ->
+    ctx = ctx' ->
+    w = w' ->
+    not_done w ->
+    <[ {instr_exp_erased (YPlus (YLit x) (YLit y)) ctx},
+       w |= AX done= {(value, ctx')} w' ]>.
+Proof.
+  intros; subst.
+  unfold_erased_expression.
+  repeat rewrite subst_ret_l.
+  cbn.
+  rewrite interp_state_ret.
+  now apply axr_ret.
+Qed.
+
+Lemma axr_yexp_yminus_ylit_ylit : forall x y value ctx ctx' w w',
+    value = (x - y)%nat ->
+    ctx = ctx' ->
+    w = w' ->
+    not_done w ->
+    <[ {instr_exp_erased (YMinus (YLit x) (YLit y)) ctx},
+       w |= AX done= {(value, ctx')} w' ]>.
+Proof.
+  intros; subst.
+  unfold_erased_expression.
+  repeat rewrite subst_ret_l.
+  cbn.
+  rewrite interp_state_ret.
+  now apply axr_ret.
+Qed.
+
+Lemma axr_yexp_ymult_ylit_ylit : forall x y value ctx ctx' w w',
+    value = (x * y)%nat ->
+    ctx = ctx' ->
+    w = w' ->
+    not_done w ->
+    <[ {instr_exp_erased (YMult (YLit x) (YLit y)) ctx},
+       w |= AX done= {(value, ctx')} w' ]>.
+Proof.
+  intros; subst.
+  unfold_erased_expression.
+  repeat rewrite subst_ret_l.
+  cbn.
+  rewrite interp_state_ret.
+  now apply axr_ret.
+Qed.
+
+Lemma axr_ystmt_yskip_erased : forall ctx ctx' w w',
+    ctx = ctx' ->
+    w = w' ->
+    not_done w ->
+    <[ {instr_stmt_erased YSkip ctx},
+       w |= AX done= {(tt, ctx')} w' ]>.
+Proof.
+  intros; subst.
+  unfold_erased_statement.
+  step_erased_state.
+  rewrite interp_state_ret.
+  now apply axr_ret.
+Qed.
+
+Lemma axax_ystmt_yyield_erased : forall ctx ctx' w w',
+    ctx = ctx' ->
+    w = w' ->
+    not_done w ->
+    <[ {instr_stmt_erased YYield ctx},
+       w |= AX AX done= {(tt, ctx')} w' ]>.
+Proof.
+  intros; subst.
+  unfold_erased_statement.
+  step_erased_state.
+  rewrite bind_ret_l.
+  cbn.
+  step_erased_state.
+  step_erased_state.
+  apply anr_state_br; split.
+  - csplit; auto.
+  - intro i; dependent destruction i.
+    + step_erased_state3.
+      rewrite interp_state_ret.
+      apply axr_ret; auto.
+    + inversion i.
+Qed.
+
+Lemma aur_ystmt_yyield_erased : forall ctx ctx' w w' ψ,
+    ctx = ctx' ->
+    w = w' ->
+    not_done w ->
+    <[ {instr_stmt_erased YYield ctx},
+       w |= ψ AU AX AX done= {(tt, ctx')} w' ]>.
+Proof.
+  intros; subst.
+  cleft.
+  now apply axax_ystmt_yyield_erased.
+Qed.
+
+Local Definition yassign_after_value
+    (name : var) (value : nat) : ictree YEff YStmtFlow :=
+  ctx <- yget;; yput (add name value ctx);; Ret Fallthrough.
+
+Local Lemma aur_yassign_after_value : forall name value ctx w ψ R,
+    <( {log (add name value ctx)}, w |= ψ )> ->
+    R (Fallthrough, add name value ctx)
+      (Obs (Log (add name value ctx)) tt) ->
+    <[ {instr_stateE (interp_thread (yassign_after_value name value)) ctx},
+       w |= ψ AU AX done R ]>.
+Proof.
+  intros name value ctx w ψ R Hlog HR.
+  pose proof (ticll_not_done unit _ _ _ Hlog) as Hnd.
+  unfold yassign_after_value, interp_thread, interp_yield, instr_stateE.
+  cbn.
+  setoid_rewrite unfold_interp.
+  cbn.
+  eapply aur_state_bind_r_eq.
+  - apply aur_get; auto; split; reflexivity.
+  - cbn.
+    expose_erased_get_result ctx.
+    eapply aur_state_bind_r_eq.
+    + apply aur_put; auto; split; reflexivity.
+    + cbn.
+      step_erased_state.
+      step_erased_state.
+      rewrite interp_state_ret.
+      cleft.
+      apply axr_ret; auto.
+      constructor.
+Qed.
+
+Local Lemma aul_yassign_after_value : forall name value ctx w ψ φ,
+    <( {log (add name value ctx)}, w |= ψ )> ->
+    <( {Ret (Fallthrough, add name value ctx)},
+       {Obs (Log (add name value ctx)) tt} |= φ )> ->
+    <( {instr_stateE (interp_thread (yassign_after_value name value)) ctx},
+       w |= ψ AU φ )>.
+Proof.
+  intros name value ctx w ψ φ Hlog Hret.
+  pose proof (ticll_not_done unit _ _ _ Hlog) as Hnd.
+  unfold yassign_after_value, interp_thread, interp_yield, instr_stateE.
+  cbn.
+  setoid_rewrite unfold_interp.
+  cbn.
+  eapply aul_state_bind_r_eq.
+  - apply aur_get; auto; split; reflexivity.
+  - cbn.
+    expose_erased_get_result ctx.
+    eapply aul_state_bind_r_eq.
+    + apply aur_put; auto; split; reflexivity.
+    + cbn.
+      step_erased_state.
+      step_erased_state.
+      rewrite interp_state_ret.
+      cleft.
+      exact Hret.
+Qed.
+
+Lemma aur_ystmt_yassign : forall name expr value ctx w ψ R,
+    <[ {instr_exp_erased expr ctx}, w |= AX done= {(value, ctx)} w ]> ->
+    <( {log (add name value ctx)}, w |= ψ )> ->
+    R (Fallthrough, add name value ctx)
+      (Obs (Log (add name value ctx)) tt) ->
+    <[ {instr_stmt_flow_erased (YAssign name expr) ctx},
+       w |= ψ AU AX done R ]>.
+Proof.
+  intros name expr value ctx w ψ R Hexp Hlog HR.
+  unfold instr_stmt_flow_erased, instr_exp_erased, interp_thread,
+    interp_yield, instr_stateE in *.
+  cbn.
+  rewrite !interp_bind_hetero.
+  rewrite !interp_state_bind.
+  eapply aur_bind_r_eq.
+  - cleft.
+    exact Hexp.
+  - cbn.
+    change (interp_state h_stateW
+              (interp handle_yield
+                 (interp handle_thread
+                    (ctx <- yget;; yput (add name value ctx);;
+                     Ret Fallthrough))) ctx)
+      with (instr_stateE (interp_thread (yassign_after_value name value)) ctx).
+    now apply aur_yassign_after_value.
+Qed.
+
+Lemma aul_ystmt_yassign : forall name expr value ctx w ψ φ,
+    <[ {instr_exp_erased expr ctx}, w |= AX done= {(value, ctx)} w ]> ->
+    <( {log (add name value ctx)}, w |= ψ )> ->
+    <( {Ret (Fallthrough, add name value ctx)},
+       {Obs (Log (add name value ctx)) tt} |= φ )> ->
+    <( {instr_stmt_flow_erased (YAssign name expr) ctx}, w |= ψ AU φ )>.
+Proof.
+  intros name expr value ctx w ψ φ Hexp Hlog Hret.
+  unfold instr_stmt_flow_erased, instr_exp_erased, interp_thread,
+    interp_yield, instr_stateE in *.
+  cbn.
+  rewrite !interp_bind_hetero.
+  rewrite !interp_state_bind.
+  eapply aul_bind_r_eq.
+  - cleft.
+    exact Hexp.
+  - cbn.
+    change (interp_state h_stateW
+              (interp handle_yield
+                 (interp handle_thread
+                    (ctx <- yget;; yput (add name value ctx);;
+                     Ret Fallthrough))) ctx)
+      with (instr_stateE (interp_thread (yassign_after_value name value)) ctx).
+    now apply aul_yassign_after_value.
+Qed.
+
+Lemma anr_ystmt_yseq_fallthrough : forall a b ctx ctx' w w' φ ψ,
+    <[ {instr_stmt_flow_erased a ctx},
+       w |= φ AN done= {(Fallthrough, ctx')} w' ]> ->
+    <[ {instr_stmt_flow_erased b ctx'}, w' |= φ AN ψ ]> ->
+    <[ {instr_stmt_flow_erased (YSeq a b) ctx}, w |= φ AN ψ ]>.
+Proof.
+  intros a b ctx ctx' w w' φ ψ Ha Hb.
+  unfold instr_stmt_flow_erased, interp_thread, interp_yield, instr_stateE in *.
+  cbn.
+  rewrite !interp_bind_hetero.
+  rewrite !interp_state_bind.
+  eapply anr_bind_r_eq; eauto.
+Qed.
+
+Lemma aur_ystmt_yseq_fallthrough : forall a b ctx ctx' w w' φ ψ,
+    <[ {instr_stmt_flow_erased a ctx},
+       w |= φ AU AX done= {(Fallthrough, ctx')} w' ]> ->
+    <[ {instr_stmt_flow_erased b ctx'}, w' |= φ AU ψ ]> ->
+    <[ {instr_stmt_flow_erased (YSeq a b) ctx}, w |= φ AU ψ ]>.
+Proof.
+  intros a b ctx ctx' w w' φ ψ Ha Hb.
+  unfold instr_stmt_flow_erased, interp_thread, interp_yield, instr_stateE in *.
+  cbn.
+  rewrite !interp_bind_hetero.
+  rewrite !interp_state_bind.
+  eapply aur_bind_r_eq; eauto.
+Qed.
+
+Lemma aul_ystmt_yseq_fallthrough : forall a b ctx ctx' w w' φ ψ,
+    <[ {instr_stmt_flow_erased a ctx},
+       w |= φ AU AX done= {(Fallthrough, ctx')} w' ]> ->
+    <( {instr_stmt_flow_erased b ctx'}, w' |= φ AU ψ )> ->
+    <( {instr_stmt_flow_erased (YSeq a b) ctx}, w |= φ AU ψ )>.
+Proof.
+  intros a b ctx ctx' w w' φ ψ Ha Hb.
+  unfold instr_stmt_flow_erased, interp_thread, interp_yield, instr_stateE in *.
+  cbn.
+  rewrite !interp_bind_hetero.
+  rewrite !interp_state_bind.
+  eapply aul_bind_r_eq; eauto.
+Qed.
+
+Lemma yseq_halt_propagates : forall a b ctx ctx' w w' φ,
+    <[ {instr_stmt_flow_erased a ctx},
+       w |= φ AU AX done= {(HaltThread, ctx')} w' ]> ->
+    not_done w' ->
+    <[ {instr_stmt_flow_erased (YSeq a b) ctx},
+       w |= φ AU AX done= {(HaltThread, ctx')} w' ]>.
+Proof.
+  intros a b ctx ctx' w w' φ Ha Hnd.
+  unfold instr_stmt_flow_erased, interp_thread, interp_yield, instr_stateE in *.
+  cbn.
+  rewrite !interp_bind_hetero.
+  rewrite !interp_state_bind.
+  eapply aur_bind_r_eq.
+  - exact Ha.
+  - cbn.
+    rewrite !unfold_interp.
+    cbn.
+    apply aur_state_ret; auto; split; reflexivity.
+Qed.
+
+Lemma aul_ystmt_yif : forall test then_branch else_branch condition ctx w φ ψ,
+    <[ {instr_exp_erased test ctx}, w |= AX done= {(condition, ctx)} w ]> ->
+    (if YieldSyntax.is_true condition then
+       <( {instr_stmt_flow_erased then_branch ctx}, w |= φ AU ψ )>
+     else
+       <( {instr_stmt_flow_erased else_branch ctx}, w |= φ AU ψ )>) ->
+    <( {instr_stmt_flow_erased (YIf test then_branch else_branch) ctx},
+       w |= φ AU ψ )>.
+Proof.
+  intros test then_branch else_branch condition ctx w φ ψ Htest Hbranch.
+  unfold instr_stmt_flow_erased, instr_exp_erased, interp_thread,
+    interp_yield, instr_stateE in *.
+  cbn.
+  rewrite !interp_bind_hetero.
+  rewrite !interp_state_bind.
+  eapply aul_bind_r_eq.
+  - cleft; exact Htest.
+  - cbn.
+    destruct (YieldSyntax.is_true condition); exact Hbranch.
+Qed.
+
+Lemma aur_ystmt_yif : forall test then_branch else_branch condition ctx w φ ψ,
+    <[ {instr_exp_erased test ctx}, w |= AX done= {(condition, ctx)} w ]> ->
+    (if YieldSyntax.is_true condition then
+       <[ {instr_stmt_flow_erased then_branch ctx}, w |= φ AU ψ ]>
+     else
+       <[ {instr_stmt_flow_erased else_branch ctx}, w |= φ AU ψ ]>) ->
+    <[ {instr_stmt_flow_erased (YIf test then_branch else_branch) ctx},
+       w |= φ AU ψ ]>.
+Proof.
+  intros test then_branch else_branch condition ctx w φ ψ Htest Hbranch.
+  unfold instr_stmt_flow_erased, instr_exp_erased, interp_thread,
+    interp_yield, instr_stateE in *.
+  cbn.
+  rewrite !interp_bind_hetero.
+  rewrite !interp_state_bind.
+  eapply aur_bind_r_eq.
+  - cleft; exact Htest.
+  - cbn.
+    destruct (YieldSyntax.is_true condition); exact Hbranch.
+Qed.
+
+(** Raw source-flow while unrolling facts.  These expose [YStmtFlow]
+    directly, avoiding any claim that the scheduled erased unit layer can
+    distinguish loop fallthrough from child-thread halt. *)
+Definition ywhile_iteration (test : YExp) (body : YStmt) :
+    ictree YEff (unit + YStmtFlow) :=
+  condition_value <- denote_exp test;;
+  if YieldSyntax.is_true condition_value then
+    flow <- denote_stmt_flow body;;
+    match flow with
+    | Fallthrough => Ret (inl tt)
+    | HaltThread => Ret (inr HaltThread)
+    end
+  else
+    Ret (inr Fallthrough).
+
+Lemma aul_ystmt_ywhile_true : forall test body condition w w' φ ψ,
+    <[ {denote_exp test}, w |= φ AU AX done= condition w ]> ->
+    YieldSyntax.is_true condition = true ->
+    <[ {denote_stmt_flow body},
+       w |= φ AU AX done= Fallthrough w' ]> ->
+    not_done w' ->
+    <( {denote_stmt_flow (YWhile test body)}, w' |= φ AU ψ )> ->
+    <( {denote_stmt_flow (YWhile test body)}, w |= φ AU ψ )>.
+Proof.
+  intros test body condition w w' φ ψ Htest Htrue Hbody Hnd Hloop.
+  cbn.
+  eapply aul_iter_next with (R := fun (_ : unit) w0 => w0 = w').
+  - eapply aur_bind_r_eq.
+    + exact Htest.
+    + rewrite Htrue.
+      eapply aur_bind_r_eq.
+      * exact Hbody.
+      * cbn.
+        cleft.
+        apply axr_ret; auto.
+        exists tt; split; auto.
+  - intros [] w0 ->.
+    exact Hloop.
+Qed.
+
+Lemma aul_ystmt_ywhile_false : forall test body condition w φ ψ,
+    <[ {denote_exp test}, w |= φ AU AX done= condition w ]> ->
+    YieldSyntax.is_true condition = false ->
+    <( {Ret Fallthrough}, w |= ψ )> ->
+    <( {denote_stmt_flow (YWhile test body)}, w |= φ AU ψ )>.
+Proof.
+  intros test body condition w φ ψ Htest Hfalse Hret.
+  pose proof Htest as Htest_not_done.
+  apply aur_not_done in Htest_not_done.
+  cbn.
+  rewrite unfold_iter.
+  eapply aul_bind_r_eq.
+  - eapply aur_bind_r_eq.
+    + exact Htest.
+    + rewrite Hfalse.
+      cbn.
+      cleft.
+      apply axr_ret.
+      * exact Htest_not_done.
+      * split; reflexivity.
+  - cbn.
+    cleft.
+    exact Hret.
+Qed.
+
+Lemma aul_ystmt_ywhile_halt : forall test body condition w w' φ ψ,
+    <[ {denote_exp test}, w |= φ AU AX done= condition w ]> ->
+    YieldSyntax.is_true condition = true ->
+    <[ {denote_stmt_flow body},
+       w |= φ AU AX done= HaltThread w' ]> ->
+    not_done w' ->
+    <( {Ret HaltThread}, w' |= ψ )> ->
+    <( {denote_stmt_flow (YWhile test body)}, w |= φ AU ψ )>.
+Proof.
+  intros test body condition w w' φ ψ Htest Htrue Hbody Hnd Hret.
+  cbn.
+  rewrite unfold_iter.
+  eapply aul_bind_r_eq.
+  - eapply aur_bind_r_eq.
+    + exact Htest.
+    + rewrite Htrue.
+      eapply aur_bind_r_eq.
+      * exact Hbody.
+      * cbn.
+        cleft.
+        apply axr_ret; auto.
+  - cbn.
+    cleft.
+    exact Hret.
+Qed.
+
+Lemma aur_ystmt_ywhile_true : forall test body condition w w' φ ψ,
+    <[ {denote_exp test}, w |= φ AU AX done= condition w ]> ->
+    YieldSyntax.is_true condition = true ->
+    <[ {denote_stmt_flow body},
+       w |= φ AU AX done= Fallthrough w' ]> ->
+    not_done w' ->
+    <[ {denote_stmt_flow (YWhile test body)}, w' |= φ AU AX ψ ]> ->
+    <[ {denote_stmt_flow (YWhile test body)}, w |= φ AU AX ψ ]>.
+Proof.
+  intros test body condition w w' φ ψ Htest Htrue Hbody Hnd Hloop.
+  cbn.
+  eapply aur_iter_next with (R := fun (_ : unit) w0 => w0 = w').
+  - eapply aur_bind_r_eq.
+    + exact Htest.
+    + rewrite Htrue.
+      eapply aur_bind_r_eq.
+      * exact Hbody.
+      * cbn.
+        cleft.
+        apply axr_ret; auto.
+        exists tt; split; auto.
+  - intros [] w0 ->.
+    exact Hloop.
+Qed.
+
+Lemma aur_ystmt_ywhile_false : forall test body condition w φ ψ,
+    <[ {denote_exp test}, w |= φ AU AX done= condition w ]> ->
+    YieldSyntax.is_true condition = false ->
+    <[ {Ret Fallthrough}, w |= AX ψ ]> ->
+    <[ {denote_stmt_flow (YWhile test body)}, w |= φ AU AX ψ ]>.
+Proof.
+  intros test body condition w φ ψ Htest Hfalse Hret.
+  pose proof Htest as Htest_not_done.
+  apply aur_not_done in Htest_not_done.
+  cbn.
+  rewrite unfold_iter.
+  eapply aur_bind_r_eq.
+  - eapply aur_bind_r_eq.
+    + exact Htest.
+    + rewrite Hfalse.
+      cbn.
+      cleft.
+      apply axr_ret.
+      * exact Htest_not_done.
+      * split; reflexivity.
+  - cbn.
+    cleft.
+    exact Hret.
+Qed.
+
+Lemma ag_ystmt_ywhile : forall test body (R : World YEff -> Prop) w φ,
+    R w ->
+    (forall w,
+        R w ->
+        <( {denote_stmt_flow (YWhile test body)}, w |= φ )> /\
+        <[ {ywhile_iteration test body}, w |= AX (φ AU AX done
+             {fun lr w' => exists i' : unit, lr = inl i' /\ R w'}) ]>) ->
+    <( {denote_stmt_flow (YWhile test body)}, w |= AG φ )>.
+Proof.
+  intros test body R w φ HR Hstep.
+  cbn.
+  change (ICtree.iter (fun _ : unit => ywhile_iteration test body) tt)
+    with (denote_stmt_flow (YWhile test body)).
+  eapply ag_iter with (R := fun (_ : unit) w => R w); eauto.
+  intros [] w0 HR0.
+  specialize (Hstep w0 HR0) as [Hφ Hnext].
+  split.
+  - exact Hφ.
+  - cbn.
+    exact Hnext.
+Qed.
+
+Lemma aur_ystmt_yassign_ylit_erased : forall name n ctx w ψ R,
+    <( {log (add name n ctx)}, w |= ψ )> ->
+    R (tt, add name n ctx) (Obs (Log (add name n ctx)) tt) ->
+    <[ {instr_stmt_erased (YAssign name (YLit n)) ctx},
+       w |= ψ AU AX done R ]>.
+Proof.
+  intros name n ctx w ψ R Hlog HR.
+  pose proof (ticll_not_done unit _ _ _ Hlog) as Hnd.
+  unfold_erased_statement.
+  eapply aur_state_bind_r_eq.
+  - apply aur_get; auto; split; reflexivity.
+  - cbn.
+    expose_erased_get_result ctx.
+    eapply aur_state_bind_r_eq.
+    + apply aur_put.
+      * exact Hlog.
+      * split; reflexivity.
+    + cbn.
+      step_erased_state3.
+      apply aur_state_ret; auto with ticl.
+Qed.
+
+Lemma aul_ystmt_yassign_ylit_erased : forall name n ctx w ψ φ,
+    <( {log (add name n ctx)}, w |= ψ )> ->
+    <( {Ret (tt, add name n ctx)},
+       {Obs (Log (add name n ctx)) tt} |= φ )> ->
+    <( {instr_stmt_erased (YAssign name (YLit n)) ctx}, w |= ψ AU φ )>.
+Proof.
+  intros name n ctx w ψ φ Hlog Hret.
+  pose proof (ticll_not_done unit _ _ _ Hlog) as Hnd.
+  unfold_erased_statement.
+  eapply aul_state_bind_r_eq.
+  - apply aur_get; auto; split; reflexivity.
+  - cbn.
+    expose_erased_get_result ctx.
+    eapply aul_state_bind_r_eq.
+    + apply aur_put.
+      * exact Hlog.
+      * split; reflexivity.
+    + cbn.
+      step_erased_state3.
+      apply aul_state_ret; auto with ticl.
+Qed.
+
+(** Scheduler one-step/case regression facts. *)
+Section SchedulerFacts.
+  Context {E : Type} `{Encode E}.
+
+  Local Ltac solve_focused_schedule H :=
+    lazy [schedule observe _observe];
+    match type of H with
+    | observe (?v ?i) = _ =>
+        change (@_observe _ _ unit (v i)) with (observe (v i));
+        rewrite H;
+        reflexivity
+    end.
+
+  Lemma schedule_empty_none (v : pool E 0) :
+    observe (schedule 0 v None) = RetF tt.
+  Proof. reflexivity. Qed.
+
+  Lemma schedule_no_focus_nonempty n (v : pool E (S n)) :
+    observe (schedule (S n) v None) =
+      VisF (inl Yield) (fun _ => Br n (fun i => schedule (S n) v (Some i))).
+  Proof. reflexivity. Qed.
+
+  Lemma schedule_focused_ret n (v : pool E (S n)) (i : Fin.t (S n)) :
+    observe (v i) = RetF tt ->
+    observe (schedule (S n) v (Some i)) =
+      GuardF (schedule n (remove_pool v i) None).
+  Proof.
+    intro Hret.
+    solve_focused_schedule Hret.
+  Qed.
+
+  Lemma schedule_focused_br n (v : pool E (S n)) (i : Fin.t (S n)) b k :
+    observe (v i) = BrF b k ->
+    observe (schedule (S n) v (Some i)) =
+      BrF b (fun j => schedule (S n) (replace_pool v i (k j)) (Some i)).
+  Proof.
+    intro Hbr.
+    solve_focused_schedule Hbr.
+  Qed.
+
+  Lemma schedule_focused_guard n (v : pool E (S n)) (i : Fin.t (S n)) t :
+    observe (v i) = GuardF t ->
+    observe (schedule (S n) v (Some i)) =
+      GuardF (schedule (S n) (replace_pool v i t) (Some i)).
+  Proof.
+    intro Hg.
+    solve_focused_schedule Hg.
+  Qed.
+
+  Lemma schedule_focused_yield n (v : pool E (S n)) (i : Fin.t (S n)) k :
+    observe (v i) = VisF (inl Yield) k ->
+    observe (schedule (S n) v (Some i)) =
+      GuardF (schedule (S n) (replace_pool v i (k tt)) None).
+  Proof.
+    intro Hy.
+    solve_focused_schedule Hy.
+  Qed.
+
+  Lemma schedule_focused_fork n (v : pool E (S n)) (i : Fin.t (S n)) k :
+    observe (v i) = VisF (inr (inl Fork)) k ->
+    observe (schedule (S n) v (Some i)) =
+      VisF ((inr (inl Spawn)) : yieldE + (spawnE + E))
+        (fun _ => schedule (S (S n))
+                    (cons_pool (k true) (replace_pool v i (k false)))
+                    (Some (Fin.FS i))).
+  Proof.
+    intro Hf.
+    solve_focused_schedule Hf.
+  Qed.
+
+  Lemma schedule_focused_user_event n (v : pool E (S n)) (i : Fin.t (S n)) e k :
+    observe (v i) = VisF (inr (inr e)) k ->
+    observe (schedule (S n) v (Some i)) =
+      VisF ((inr (inr e)) : yieldE + (spawnE + E))
+        (fun x => schedule (S n) (replace_pool v i (k x)) (Some i)).
+  Proof.
+    intro Hu.
+    solve_focused_schedule Hu.
+  Qed.
+End SchedulerFacts.
+
+(** Non-degenerate finite-pool scheduler regressions. *)
+Section SchedulerPoolRegressions.
+  Context {E : Type} `{Encode E}.
+
+  Lemma schedule_yield_two_threads_one_step (next other : thread E) :
+    observe
+      (schedule 2
+         (cons_pool
+            (Vis ((inl Yield) : yieldE + (forkE + E)) (fun _ : unit => next))
+            (fun _ : Fin.t 1 => other))
+         (Some Fin.F1)) =
+      GuardF
+        (schedule 2
+           (replace_pool
+              (cons_pool
+                 (Vis ((inl Yield) : yieldE + (forkE + E)) (fun _ : unit => next))
+                 (fun _ : Fin.t 1 => other))
+              Fin.F1 next)
+           None).
+  Proof. reflexivity. Qed.
+
+  Lemma schedule_yield_two_threads_focused_slot (next other : thread E) :
+    replace_pool
+      (cons_pool
+         (Vis ((inl Yield) : yieldE + (forkE + E)) (fun _ : unit => next))
+         (fun _ : Fin.t 1 => other))
+      Fin.F1 next Fin.F1 = next.
+  Proof. apply replace_pool_hit. Qed.
+
+  Lemma schedule_yield_two_threads_other_slot (next other : thread E) :
+    replace_pool
+      (cons_pool
+         (Vis ((inl Yield) : yieldE + (forkE + E)) (fun _ : unit => next))
+         (fun _ : Fin.t 1 => other))
+      Fin.F1 next (Fin.FS Fin.F1) = other.
+  Proof.
+    rewrite replace_pool_miss by discriminate.
+    apply cons_pool_tail.
+  Qed.
+
+  Lemma schedule_fork_two_threads_one_step
+      (child parent other : thread E) :
+    observe
+      (schedule 2
+         (cons_pool
+            (Vis ((inr (inl Fork)) : yieldE + (forkE + E))
+               (fun in_child : bool => if in_child then child else parent))
+            (fun _ : Fin.t 1 => other))
+         (Some Fin.F1)) =
+      VisF ((inr (inl Spawn)) : yieldE + (spawnE + E))
+        (fun _ =>
+           schedule 3
+             (cons_pool child
+                (replace_pool
+                   (cons_pool
+                      (Vis ((inr (inl Fork)) : yieldE + (forkE + E))
+                         (fun in_child : bool => if in_child then child else parent))
+                      (fun _ : Fin.t 1 => other))
+                   Fin.F1 parent))
+             (Some (Fin.FS Fin.F1))).
+  Proof. reflexivity. Qed.
+
+  Lemma schedule_fork_two_threads_child_slot
+      (child parent other : thread E) :
+    cons_pool child
+      (replace_pool
+         (cons_pool
+            (Vis ((inr (inl Fork)) : yieldE + (forkE + E))
+               (fun in_child : bool => if in_child then child else parent))
+            (fun _ : Fin.t 1 => other))
+         Fin.F1 parent)
+      Fin.F1 = child.
+  Proof. apply cons_pool_head. Qed.
+
+  Lemma schedule_fork_two_threads_parent_slot
+      (child parent other : thread E) :
+    cons_pool child
+      (replace_pool
+         (cons_pool
+            (Vis ((inr (inl Fork)) : yieldE + (forkE + E))
+               (fun in_child : bool => if in_child then child else parent))
+            (fun _ : Fin.t 1 => other))
+         Fin.F1 parent)
+      (Fin.FS Fin.F1) = parent.
+  Proof.
+    rewrite cons_pool_tail.
+    apply replace_pool_hit.
+  Qed.
+
+  Lemma schedule_fork_two_threads_other_slot
+      (child parent other : thread E) :
+    cons_pool child
+      (replace_pool
+         (cons_pool
+            (Vis ((inr (inl Fork)) : yieldE + (forkE + E))
+               (fun in_child : bool => if in_child then child else parent))
+            (fun _ : Fin.t 1 => other))
+         Fin.F1 parent)
+      (Fin.FS (Fin.FS Fin.F1)) = other.
+  Proof.
+    rewrite cons_pool_tail.
+    rewrite replace_pool_miss by discriminate.
+    apply cons_pool_tail.
+  Qed.
+End SchedulerPoolRegressions.
+
+(** Concrete scheduler-visible examples. *)
+Local Ltac solve_visible_regression :=
+  cbn;
+  unfold resum, ReSum_refl, resum_ret, ReSumRet_refl;
+  reflexivity.
+
+Lemma scheduled_visible_yyield_one_step :
+  observe (scheduled_visible YYield) =
+    GuardF
+      (schedule 1
+         (replace_pool
+            (fun _ : Fin.t 1 => denote_stmt YYield)
+            Fin.F1 (denote_stmt YSkip))
+         None).
+Proof.
+  unfold scheduled_visible.
+  apply (@schedule_focused_yield Mem _ 0
+           (fun _ : Fin.t 1 => denote_stmt YYield)
+           Fin.F1
+           (fun _ : unit => denote_stmt YSkip)).
+  solve_visible_regression.
+Qed.
+
+Definition yfork_body_fork_continuation
+    (body : YStmt) (in_child : bool) : thread Mem :=
+  ICtree.subst'
+    (fun _ : YStmtFlow => Ret tt)
+    (observe
+       (ICtree.subst'
+          (fun branch : bool =>
+             if branch then
+               denote_stmt_flow body;; Ret HaltThread
+             else
+               Ret Fallthrough)
+          (RetF in_child))).
+
+Lemma scheduled_visible_yfork_body_one_step : forall body,
+  observe (scheduled_visible (YFork body)) =
+    VisF ((inr (inl Spawn)) : yieldE + (spawnE + Mem))
+      (fun _ =>
+         schedule 2
+           (cons_pool (yfork_body_fork_continuation body true)
+              (replace_pool
+                 (fun _ : Fin.t 1 => denote_stmt (YFork body))
+                 Fin.F1 (yfork_body_fork_continuation body false)))
+           (Some (Fin.FS Fin.F1))).
+Proof.
+  intro body.
+  unfold scheduled_visible.
+  apply (@schedule_focused_fork Mem _ 0
+           (fun _ : Fin.t 1 => denote_stmt (YFork body))
+           Fin.F1
+           (yfork_body_fork_continuation body)).
+  solve_visible_regression.
+Qed.
+
+Lemma yfork_child_halts_after_body body :
+  yfork_body_fork_continuation body true =
+    ICtree.subst' (fun _ : YStmtFlow => Ret tt)
+      (observe (denote_stmt_flow body;; Ret HaltThread)).
+Proof. reflexivity. Qed.
+
+Lemma yfork_parent_falls_through body :
+  observe (yfork_body_fork_continuation body false) = RetF tt.
+Proof. solve_visible_regression. Qed.
+
+Definition yseq_yfork_body_rest_fork_continuation
+    (body rest : YStmt) (in_child : bool) : thread Mem :=
+  ICtree.subst'
+    (fun _ : YStmtFlow => Ret tt)
+    (observe
+       (ICtree.subst'
+          (fun flow : YStmtFlow =>
+             match flow with
+             | Fallthrough => denote_stmt_flow rest
+             | HaltThread => Ret HaltThread
+             end)
+          (observe
+             (ICtree.subst'
+                (fun branch : bool =>
+                   if branch then
+                     denote_stmt_flow body;; Ret HaltThread
+                   else
+                     Ret Fallthrough)
+                (RetF in_child))))).
+
+Lemma scheduled_visible_yseq_yfork_body_rest_one_step : forall body rest,
+  observe (scheduled_visible (YSeq (YFork body) rest)) =
+    VisF ((inr (inl Spawn)) : yieldE + (spawnE + Mem))
+      (fun _ =>
+         schedule 2
+           (cons_pool
+              (yseq_yfork_body_rest_fork_continuation body rest true)
+              (replace_pool
+                 (fun _ : Fin.t 1 =>
+                    denote_stmt (YSeq (YFork body) rest))
+                 Fin.F1
+                 (yseq_yfork_body_rest_fork_continuation body rest false)))
+           (Some (Fin.FS Fin.F1))).
+Proof.
+  intros body rest.
+  unfold scheduled_visible.
+  apply (@schedule_focused_fork Mem _ 0
+           (fun _ : Fin.t 1 => denote_stmt (YSeq (YFork body) rest))
+           Fin.F1
+           (yseq_yfork_body_rest_fork_continuation body rest)).
+  solve_visible_regression.
+Qed.
+
+Lemma yseq_yfork_body_rest_parent_runs_rest body rest :
+  observe (yseq_yfork_body_rest_fork_continuation body rest false) =
+    observe (denote_stmt rest).
+Proof. solve_visible_regression. Qed.
+
+Definition yfork_yield_fork_continuation (in_child : bool) : thread Mem :=
+  ICtree.subst'
+    (fun _ : YStmtFlow => Ret tt)
+    (observe
+       (ICtree.subst'
+          (fun branch : bool =>
+             if branch then
+               denote_stmt_flow YYield;; Ret HaltThread
+             else
+               Ret Fallthrough)
+          (RetF in_child))).
+
+Lemma scheduled_visible_yfork_yield_one_step :
+  observe (scheduled_visible (YFork YYield)) =
+    VisF ((inr (inl Spawn)) : yieldE + (spawnE + Mem))
+      (fun _ =>
+         schedule 2
+           (cons_pool (yfork_yield_fork_continuation true)
+              (replace_pool
+                 (fun _ : Fin.t 1 => denote_stmt (YFork YYield))
+                 Fin.F1 (yfork_yield_fork_continuation false)))
+           (Some (Fin.FS Fin.F1))).
+Proof.
+  unfold scheduled_visible.
+  apply (@schedule_focused_fork Mem _ 0
+           (fun _ : Fin.t 1 => denote_stmt (YFork YYield))
+           Fin.F1
+           yfork_yield_fork_continuation).
+  solve_visible_regression.
+Qed.
+
+Definition yseq_yfork_skip_yield_fork_continuation
+    (in_child : bool) : thread Mem :=
+  ICtree.subst'
+    (fun _ : YStmtFlow => Ret tt)
+    (observe
+       (ICtree.subst'
+          (fun flow : YStmtFlow =>
+             match flow with
+             | Fallthrough => denote_stmt_flow YYield
+             | HaltThread => Ret HaltThread
+             end)
+          (observe
+             (ICtree.subst'
+                (fun branch : bool =>
+                   if branch then
+                     denote_stmt_flow YSkip;; Ret HaltThread
+                   else
+                     Ret Fallthrough)
+                (RetF in_child))))).
+
+Lemma yseq_yfork_skip_yield_child_done :
+  observe (yseq_yfork_skip_yield_fork_continuation true) = RetF tt.
+Proof. solve_visible_regression. Qed.
+
+Lemma yseq_yfork_skip_yield_parent_yields :
+  observe (yseq_yfork_skip_yield_fork_continuation false) =
+    VisF ((inl Yield) : YEff) (fun _ : unit => denote_stmt YSkip).
+Proof. solve_visible_regression. Qed.
+
+Lemma scheduled_visible_yseq_yfork_skip_yield_one_step :
+  observe (scheduled_visible (YSeq (YFork YSkip) YYield)) =
+    VisF ((inr (inl Spawn)) : yieldE + (spawnE + Mem))
+      (fun _ =>
+         schedule 2
+           (cons_pool (yseq_yfork_skip_yield_fork_continuation true)
+              (replace_pool
+                 (fun _ : Fin.t 1 =>
+                    denote_stmt (YSeq (YFork YSkip) YYield))
+                 Fin.F1 (yseq_yfork_skip_yield_fork_continuation false)))
+           (Some (Fin.FS Fin.F1))).
+Proof.
+  unfold scheduled_visible.
+  apply (@schedule_focused_fork Mem _ 0
+           (fun _ : Fin.t 1 => denote_stmt (YSeq (YFork YSkip) YYield))
+           Fin.F1
+           yseq_yfork_skip_yield_fork_continuation).
+  solve_visible_regression.
+Qed.
+
+(** Erasure handlers intentionally hide scheduler/thread observations. *)
+Lemma handle_spawn_spawn_erased : handle_spawn (inr (inl Spawn)) = Ret tt.
+Proof. reflexivity. Qed.
+
+Lemma handle_yield_yield_erased : handle_yield (inl Yield) = Ret tt.
+Proof. reflexivity. Qed.
+
+Lemma interp_scheduled_erased_unfold s :
+  interp_scheduled_erased s = interp_yield (interp_spawn (scheduled_visible s)).
+Proof. reflexivity. Qed.
+
+(** Compatibility aliases are erased APIs. *)
+Lemma scheduled_alias s : scheduled s = scheduled_visible s.
+Proof. reflexivity. Qed.
+
+Lemma interp_scheduled_alias_erased s : interp_scheduled s = interp_scheduled_erased s.
+Proof. reflexivity. Qed.
+
+Lemma instr_exp_alias_erased e ctx : instr_exp e ctx = instr_exp_erased e ctx.
+Proof. reflexivity. Qed.
+
+Lemma instr_stmt_alias_erased s ctx : instr_stmt s ctx = instr_stmt_erased s ctx.
+Proof. reflexivity. Qed.
diff --git a/theories/Lang/Yield/Vec.v b/theories/Lang/Yield/Vec.v
new file mode 100644
index 0000000..5797dad
--- /dev/null
+++ b/theories/Lang/Yield/Vec.v
@@ -0,0 +1,55 @@
+From Stdlib Require Import Fin.
+
+(** Replace the value stored at one finite index. *)
+Definition replace_pool {A n} (v : Fin.t n -> A) (i : Fin.t n) (a : A) : Fin.t n -> A :=
+  fun j =>
+    match Fin.eq_dec i j with
+    | left _ => a
+    | right _ => v j
+    end.
+
+Lemma replace_pool_hit {A n} (v : Fin.t n -> A) (i : Fin.t n) (a : A) :
+  replace_pool v i a i = a.
+Proof.
+  unfold replace_pool.
+  destruct (Fin.eq_dec i i) as [_ | Hneq].
+  - reflexivity.
+  - contradiction Hneq; reflexivity.
+Qed.
+
+Lemma replace_pool_miss {A n} (v : Fin.t n -> A) (i j : Fin.t n) (a : A) :
+  i <> j -> replace_pool v i a j = v j.
+Proof.
+  intro Hneq.
+  unfold replace_pool.
+  destruct (Fin.eq_dec i j) as [Heq | _].
+  - contradiction Hneq; exact Heq.
+  - reflexivity.
+Qed.
+
+(** Remove one index from a non-empty finite vector/function. *)
+Fixpoint remove_pool {A} {n : nat} : (Fin.t (S n) -> A) -> Fin.t (S n) -> Fin.t n -> A :=
+  match n return (Fin.t (S n) -> A) -> Fin.t (S n) -> Fin.t n -> A with
+  | 0 => fun _ _ j => match j with end
+  | S n' => fun v i j =>
+      match i in Fin.t (S n0) return n0 = S n' -> Fin.t (S n') -> A with
+      | F1 => fun _ j => v (FS j)
+      | FS i' => fun e j =>
+          match j in Fin.t (S n1) return n1 = n' -> A with
+          | F1 => fun _ => v F1
+          | FS j' => fun e' => remove_pool (fun k => v (FS k)) (Fin.cast i' e) (Fin.cast j' e')
+          end eq_refl
+      end eq_refl j
+  end.
+
+(** Prepend a value at [F1] and shift the existing pool right. *)
+Definition cons_pool {A n} (x : A) (v : Fin.t n -> A) : Fin.t (S n) -> A :=
+  fun i => Fin.caseS' i (fun _ => A) x (fun j => v j).
+
+Lemma cons_pool_head {A n} (x : A) (v : Fin.t n -> A) :
+  cons_pool x v Fin.F1 = x.
+Proof. reflexivity. Qed.
+
+Lemma cons_pool_tail {A n} (x : A) (v : Fin.t n -> A) (i : Fin.t n) :
+  cons_pool x v (Fin.FS i) = v i.
+Proof. reflexivity. Qed.