diff --git a/DESIGN.md b/DESIGN.md
index afa954a..67b5e19 100644
--- a/DESIGN.md
+++ b/DESIGN.md
@@ -59,6 +59,17 @@ Following Iris, specifications are stated with a weakest-precondition predicate
 that the initial and final distributions refine (`Framed`): the part of the state that
 satisfies the invariant is any space `𝓙` with `⌈I⌉ 𝓙`, as in `P ⊨ φ ∗ ⌈I⌉`.
 
+The paper runs programs on memories with a fixed domain. Here memories are partial, so
+`wp` states two facts that the paper gets for free:
+
+- the postcondition space owns no variables beyond those of the precondition space
+  (`𝓠.dom ⊆ 𝓟.dom`); this is what makes the postconditions of two parallel threads
+  independent;
+- the program does not deallocate variables (`Distr.Keeps μ ν`: every variable that is
+  allocated in all initial memories is allocated in all final memories). The postcondition
+  space may be smaller than the precondition space, so without this fact the branches of an
+  outcome conjunction could not be brought back to a common domain (`Split`).
+
 ## Invariants
 
 Invariants are ordered by factorization (`Inv.LE_Inv`): `𝓘 ≤ 𝓙` when `𝓘` is `𝓙 ∗ 𝓚` for
diff --git a/PcolIris/Examples/VonNeumann.lean b/PcolIris/Examples/VonNeumann.lean
index 6247bf6..6507119 100644
--- a/PcolIris/Examples/VonNeumann.lean
+++ b/PcolIris/Examples/VonNeumann.lean
@@ -341,8 +341,17 @@ same defect that the development itself documents for `sum_prod_distribute`. -/
 /-- **Introduction of a nondeterministic choice**: every branch of a nondeterministic choice
 entails the choice itself.  (In the semantics of the paper `&` is a union of sets of
 probability spaces, so this is immediate.) -/
-lemma nondet_intro {iota : Type} [Countable iota] {phi : iota → OProp} (i : iota) : phi i ⊢ OProp.nondet phi :=
-  sorry
+lemma nondet_intro {iota : Type} [Countable iota] {phi : iota → OProp} (i : iota) :
+    phi i ⊢ OProp.nondet phi := by
+  intro 𝓟 h
+  obtain ⟨code, hcode⟩ := Countable.exists_injective_nat iota
+  refine ⟨PMF.pure i, fun v ↦ 𝓟.shift (code v), 𝓟.dom,
+    fun hij ↦ ProbSpace.disjoint_support_shift _ _ (hcode.ne hij), fun _ ↦ rfl, ?_, ?_⟩
+  · exact (ProbSpace.sum_pure_le _ _ i).trans (ProbSpace.shift_le _ _)
+  · intro v hv
+    rw [PMF.support_pure, Set.mem_singleton_iff] at hv
+    subst hv
+    exact (phi v).mono (ProbSpace.le_shift _ _) h
 
 /-- Nondeterministic choices are convex: a mixture of unions of mixtures is again one. -/
 lemma Convex.nondet {iota : Type} [Countable iota] {phi : iota → OProp} : Convex (OProp.nondet phi) := sorry
@@ -551,7 +560,11 @@ lemma wp_body_nondet {L : Finset ℚ} {F : ProbSpace → Prop} (eps : ℚ)
 the loop body. -/
 lemma phi1_split : phi1 ⊢ iprop(⌈own ($"p'")⌉ ∗ (⌈own ($"x")⌉ ∗ ⌈own ($"y")⌉)) :=
   Iris.BI.Entails.trans (OProp.sure_weaken phi1_resources)
-    (Iris.BI.Entails.trans OProp.sure_sep.1 (Iris.BI.sep_mono_right OProp.sure_sep.1))
+    (Iris.BI.Entails.trans
+      (OProp.sure_sep (MProp.Footprint.own_var _)
+        ((MProp.Footprint.own_var _).sep (MProp.Footprint.own_var _) (by simp))).1
+      (Iris.BI.sep_mono_right
+        (OProp.sure_sep (MProp.Footprint.own_var _) (MProp.Footprint.own_var _)).1))
 
 /-- **The loop body.**  Starting from the loop invariant at rank `1`, one iteration of the
 loop exits with probability at least `2 * eps * (1 - eps)`. -/
diff --git a/PcolIris/Logic/Framed.lean b/PcolIris/Logic/Framed.lean
index d1440ab..6e065bb 100644
--- a/PcolIris/Logic/Framed.lean
+++ b/PcolIris/Logic/Framed.lean
@@ -22,6 +22,18 @@ lemma Inv.footprint (𝓘 : Inv) : 𝓘.to_MProp.Footprint 𝓘.dom := by
   rw [Mem.restrict_dom] at this
   exact Set.inter_eq_right.mp this
 
+/-- Every memory that `ν` gives positive probability owns the variables `D`. -/
+def Distr.Owns (ν : Distr Mem) (D : Set Var) : Prop :=
+  ∀ m : Mem, ν (m : WithBot Mem) ≠ 0 → D ⊆ m.dom
+
+/-- A run from `μ` to `ν` does not deallocate variables. -/
+def Distr.Keeps (μ ν : Distr Mem) : Prop :=
+  ∀ D, Distr.Owns μ D → Distr.Owns ν D
+
+lemma Distr.Keeps.refl (μ : Distr Mem) : Distr.Keeps μ μ := fun _ h ↦ h
+
+lemma Distr.Keeps.trans {μ ν ρ : Distr Mem} (h₁ : Distr.Keeps μ ν) (h₂ : Distr.Keeps ν ρ) : Distr.Keeps μ ρ :=
+  fun D h ↦ h₂ D (h₁ D h)
 
 /--
 `Framed 𝓘 𝓟 𝓟fr 𝓙 μ` states that the distribution `μ` refines the product of a space `𝓟`
@@ -72,6 +84,21 @@ lemma right {𝓟₁ 𝓟₂ : ProbSpace} (hd : Disjoint 𝓟₁.dom 𝓟₂.dom
   have hf' : Framed 𝓘 (𝓟₂ ⊗ 𝓟₁) 𝓟fr 𝓙 μ := hf.mono hc
   exact hf'.left hd.symm
 
+/-- Moving the left factor of the frame into the program's space. -/
+lemma unright {𝓟₁ 𝓟₂ : ProbSpace} (hd₁ : Disjoint 𝓟₁.dom 𝓟fr.dom)
+    (hf : Framed 𝓘 𝓟₂ (𝓟₁ ⊗ 𝓟fr) 𝓙 μ) : Framed 𝓘 (𝓟₁ ⊗ 𝓟₂) 𝓟fr 𝓙 μ := by
+  have hd : Disjoint 𝓟₂.dom (𝓟₁.dom ∪ 𝓟fr.dom) := hf.disj_frame
+  have h₂₁ : Disjoint 𝓟₂.dom 𝓟₁.dom := (Set.disjoint_union_right.mp hd).1
+  have h₂f : Disjoint 𝓟₂.dom 𝓟fr.dom := (Set.disjoint_union_right.mp hd).2
+  refine ⟨hf.inv, Set.disjoint_union_left.mpr ⟨hd₁, h₂f⟩, ?_, ?_⟩
+  · have h := hf.disj_inv
+    change Disjoint (𝓟₂.dom ∪ (𝓟₁.dom ∪ 𝓟fr.dom)) 𝓙.dom at h
+    change Disjoint ((𝓟₁.dom ∪ 𝓟₂.dom) ∪ 𝓟fr.dom) 𝓙.dom
+    rwa [Set.union_comm 𝓟₁.dom 𝓟₂.dom, Set.union_assoc]
+  · refine Distr.Refines.mono (ProbSpace.product_mono_left ?_ hf.disj_inv) hf.refines
+    exact (ProbSpace.product_mono_left (ProbSpace.product_comm h₂₁)
+      (Set.disjoint_union_left.mpr ⟨h₂f, hd₁⟩)).trans (ProbSpace.product_assoc 𝓟₂ 𝓟₁ 𝓟fr)
+
 end Framed
 
 end Pcol
diff --git a/PcolIris/Logic/LemmaC6.lean b/PcolIris/Logic/LemmaC6.lean
index 789e7d2..a46084a 100644
--- a/PcolIris/Logic/LemmaC6.lean
+++ b/PcolIris/Logic/LemmaC6.lean
@@ -23,8 +23,9 @@ open Linearization
 invariant `𝓘`, and let `μ` be an initial distribution framed by `𝓟₁ ⊗ 𝓟₂`, a frame `𝓟fr`
 and a space `𝓙` satisfying the invariant.  If, for an arbitrary frame `𝓕`, running thread
 `k` on any distribution framed by `𝓟ₖ` and `𝓕` yields a distribution framed by `𝓠ₖ` and
-`𝓕`, then running the two threads in parallel on `μ` yields a distribution framed by
-`𝓠₁ ⊗ 𝓠₂` and `𝓟fr`.
+`𝓕` (without deallocating variables), then running the two threads in parallel on `μ`
+yields a distribution framed by `𝓠₁ ⊗ 𝓠₂` and `𝓟fr` (again without deallocating
+variables).
 
 The side conditions of the original statement (each thread only acts on the variables it
 owns, and only tests its own variables) are replaced here by the requirement that the two
@@ -39,11 +40,11 @@ theorem lemma_C6 {𝓘 : Inv} {p₁ p₂ : Pom (Label (WithInv Act) Test)}
     {𝓟₁ 𝓟₂ 𝓠₁ 𝓠₂ 𝓟fr 𝓙 : ProbSpace} {μ : Distr Mem}
     (hμ : Framed 𝓘 (𝓟₁ ⊗ 𝓟₂) 𝓟fr 𝓙 μ)
     (h₁ : ∀ (𝓕 𝓙₁ : ProbSpace) (μ₁ : Distr Mem), Framed 𝓘 𝓟₁ 𝓕 𝓙₁ μ₁ →
-      ∀ ν₁ ∈ ConvexPowerset.singleton' μ₁ >>= 𝓛 p₁, ∃ 𝓙₁', Framed 𝓘 𝓠₁ 𝓕 𝓙₁' ν₁)
+      ∀ ν₁ ∈ ConvexPowerset.singleton' μ₁ >>= 𝓛 p₁, Distr.Keeps μ₁ ν₁ ∧ ∃ 𝓙₁', Framed 𝓘 𝓠₁ 𝓕 𝓙₁' ν₁)
     (h₂ : ∀ (𝓕 𝓙₂ : ProbSpace) (μ₂ : Distr Mem), Framed 𝓘 𝓟₂ 𝓕 𝓙₂ μ₂ →
-      ∀ ν₂ ∈ ConvexPowerset.singleton' μ₂ >>= 𝓛 p₂, ∃ 𝓙₂', Framed 𝓘 𝓠₂ 𝓕 𝓙₂' ν₂) :
+      ∀ ν₂ ∈ ConvexPowerset.singleton' μ₂ >>= 𝓛 p₂, Distr.Keeps μ₂ ν₂ ∧ ∃ 𝓙₂', Framed 𝓘 𝓠₂ 𝓕 𝓙₂' ν₂) :
     ∀ ν ∈ ConvexPowerset.singleton' μ >>= 𝓛 (Pom.Semantics.par p₁ p₂),
-      ∃ 𝓙', Framed 𝓘 (𝓠₁ ⊗ 𝓠₂) 𝓟fr 𝓙' ν := by
+      Distr.Keeps μ ν ∧ ∃ 𝓙', Framed 𝓘 (𝓠₁ ⊗ 𝓠₂) 𝓟fr 𝓙' ν := by
   sorry
 
 end Pcol
diff --git a/PcolIris/Logic/WeakestPre.lean b/PcolIris/Logic/WeakestPre.lean
index 7d3c503..ebdd077 100644
--- a/PcolIris/Logic/WeakestPre.lean
+++ b/PcolIris/Logic/WeakestPre.lean
@@ -21,10 +21,14 @@ def wp_base (𝓘 : Inv) (F : ProbSpace → Prop) (c : Cmd Act) (ψ : OProp) : O
       Framed 𝓘 𝓟 𝓟fr 𝓙 μ →
       -- Take any `ν` that results from running the program
       ∀ ν ∈ ConvexPowerset.singleton' μ >>= 𝓛 (c.withInv 𝓘).to_pom,
-      -- Then `ν` refines some probability space `𝓠`, which satisfies the postcondition `ψ`,
-      -- together with the same frame and a space satisfying the invariant
-        ∃ 𝓠 𝓙', Framed 𝓘 𝓠 𝓟fr 𝓙' ν ∧ ψ 𝓠
-  upcl := fun hle h μ 𝓟fr 𝓙 hF hf ν hν ↦ h μ 𝓟fr 𝓙 hF (hf.mono hle) ν hν
+      -- Then the program has not deallocated variables, and `ν` refines some probability
+      -- space `𝓠`, which satisfies the postcondition `ψ`, together with the same frame and a
+      -- space satisfying the invariant.  The program does not acquire variables either: `𝓠`
+      -- owns no more variables than `𝓟`.
+        Distr.Keeps μ ν ∧ ∃ 𝓠 𝓙', Framed 𝓘 𝓠 𝓟fr 𝓙' ν ∧ 𝓠.dom ⊆ 𝓟.dom ∧ ψ 𝓠
+  upcl := fun hle h μ 𝓟fr 𝓙 hF hf ν hν ↦
+    let ⟨hk, 𝓠, 𝓙', hf', hdom, hψ⟩ := h μ 𝓟fr 𝓙 hF (hf.mono hle) ν hν
+    ⟨hk, 𝓠, 𝓙', hf', hdom.trans (ProbSpace.dom_mono hle), hψ⟩
 
 /-- The standard "strong" wp allows any frame -/
 def wp (𝓘 : Inv) : Cmd Act → OProp → OProp := wp_base 𝓘 (fun _ ↦ True)
@@ -40,24 +44,25 @@ notation 𝓘 " ⊢{{" φ "}} " c " {{" ψ "}}" => φ ⊢ wp 𝓘 c ψ
 
 variable {𝓘 : Inv} {F : ProbSpace → Prop} {c : Cmd Act}
 
+/-- The `Skip` rule. -/
 lemma wp_skip (φ : OProp) :
-    φ ⊣⊢ wp_base 𝓘 F Cmd.skip φ := by
-  constructor
-  · intro 𝓟 hφ μ 𝓟fr 𝓙 _ hf ν hν
-    refine ⟨𝓟, 𝓙, ?_, hφ⟩
-    rw [Cmd.withInv, Cmd.to_pom, Pom.Semantics.lin_skip, bind_pure] at hν
-    obtain ⟨μ, rfl⟩ := PMF.to_distr_inv hf.refines.bot_0
-    have heq : ν = μ.to_distr := sorry
-    rwa [heq]
-  · intro 𝓟 hφ; sorry
+    φ ⊢ wp_base 𝓘 F Cmd.skip φ := by
+  intro 𝓟 hφ μ 𝓟fr 𝓙 _ hf ν hν
+  rw [Cmd.withInv, Cmd.to_pom, Pom.Semantics.lin_skip, bind_pure] at hν
+  have hle : μ ≤ ν := by
+    have : ν ∈ (ConvexPowerset.singleton' μ).set := hν
+    rwa [ConvexPowerset.singleton'_set_eq] at this
+  rw [← proper_dist_maximal hf.refines.bot_0 hle]
+  exact ⟨Distr.Keeps.refl μ, 𝓟, 𝓙, hf, subset_rfl, hφ⟩
 
 lemma wp_seq {c₁ c₂ : Cmd Act} {ψ : OProp} :
     wp_base 𝓘 F c₁ (wp_base 𝓘 F c₂ ψ) ⊢ wp_base 𝓘 F (Cmd.seq c₁ c₂) ψ := by
   intro 𝓟 h μ 𝓟fr 𝓙 hF href ν; rw [Cmd.withInv, Cmd.to_pom, Pom.lin_seq, ← bind_assoc]
   intro hν; rcases ConvexPowerset.mem_bind.mp hν with ⟨ξ, hξ, f, hf, rfl⟩
-  have ⟨𝓡, 𝓙', href', h'⟩ := h μ 𝓟fr 𝓙 hF href ξ hξ
-  refine h' ξ 𝓟fr 𝓙' hF href' _ ?_
-  exact ConvexPowerset.mem_bind.mpr ⟨ξ, ConvexPowerset.self_mem_singleton' _, f, hf, rfl⟩
+  have ⟨hk, 𝓡, 𝓙', href', hdom, h'⟩ := h μ 𝓟fr 𝓙 hF href ξ hξ
+  obtain ⟨hk', 𝓠, 𝓙'', hf'', hdom', hψ⟩ := h' ξ 𝓟fr 𝓙' hF href' _
+    (ConvexPowerset.mem_bind.mpr ⟨ξ, ConvexPowerset.self_mem_singleton' _, f, hf, rfl⟩)
+  exact ⟨Distr.Keeps.trans hk hk', 𝓠, 𝓙'', hf'', hdom'.trans hdom, hψ⟩
 
 lemma wp_if_true {b : Expr} {c₁ c₂ : Cmd Act} {φ ψ : OProp} :
      ⌈b == Expr.literal 1⌉ ∧ wp_base 𝓘 F c₁ ψ ⊢ wp_base 𝓘 F (Cmd.if_stmt b c₁ c₂) ψ := by
@@ -122,31 +127,33 @@ lemma wp_par {𝓘 : Inv} {c₁ c₂ : Cmd Act} {ψ₁ ψ₂ : OProp}
   have hf' := hf.mono hle
   obtain ⟨ν₁, hν₁⟩ := (ConvexPowerset.singleton' μ >>= 𝓛 (c₁.withInv 𝓘).to_pom).nonempty
   obtain ⟨ν₂, hν₂⟩ := (ConvexPowerset.singleton' μ >>= 𝓛 (c₂.withInv 𝓘).to_pom).nonempty
-  obtain ⟨_, _, -, hψ₁'⟩ := h₁ μ _ 𝓙 True.intro (hf'.left hdisj) ν₁ hν₁
-  obtain ⟨_, _, -, hψ₂'⟩ := h₂ μ _ 𝓙 True.intro (hf'.right hdisj) ν₂ hν₂
+  obtain ⟨-, 𝓡₁, _, -, hdom₁, hψ₁'⟩ := h₁ μ _ 𝓙 True.intro (hf'.left hdisj) ν₁ hν₁
+  obtain ⟨-, 𝓡₂, _, -, hdom₂, hψ₂'⟩ := h₂ μ _ 𝓙 True.intro (hf'.right hdisj) ν₂ hν₂
   obtain ⟨𝓠₁, hQ₁⟩ := hψ₁ _ hψ₁'
   obtain ⟨𝓠₂, hQ₂⟩ := hψ₂ _ hψ₂'
   -- Each thread, run in isolation with an arbitrary frame, establishes its postcondition;
   -- by precision, the least such postcondition space is `𝓠ₖ`
   have hthread₁ : ∀ (𝓕 𝓙₁ : ProbSpace) (μ₁ : Distr Mem), Framed 𝓘 𝓟₁ 𝓕 𝓙₁ μ₁ →
       ∀ ν₁ ∈ ConvexPowerset.singleton' μ₁ >>= 𝓛 (c₁.withInv 𝓘).to_pom,
-        ∃ 𝓙₁', Framed 𝓘 𝓠₁ 𝓕 𝓙₁' ν₁ := by
+        Distr.Keeps μ₁ ν₁ ∧ ∃ 𝓙₁', Framed 𝓘 𝓠₁ 𝓕 𝓙₁' ν₁ := by
     intro 𝓕 𝓙₁ μ₁ hf₁ ν₁ hν₁
-    obtain ⟨𝓠, 𝓙₁', hf', hψ⟩ := h₁ μ₁ 𝓕 𝓙₁ True.intro hf₁ ν₁ hν₁
-    exact ⟨𝓙₁', hf'.mono ((hQ₁ 𝓠).mpr hψ)⟩
+    obtain ⟨hk, 𝓠, 𝓙₁', hf', -, hψ⟩ := h₁ μ₁ 𝓕 𝓙₁ True.intro hf₁ ν₁ hν₁
+    exact ⟨hk, 𝓙₁', hf'.mono ((hQ₁ 𝓠).mpr hψ)⟩
   have hthread₂ : ∀ (𝓕 𝓙₂ : ProbSpace) (μ₂ : Distr Mem), Framed 𝓘 𝓟₂ 𝓕 𝓙₂ μ₂ →
       ∀ ν₂ ∈ ConvexPowerset.singleton' μ₂ >>= 𝓛 (c₂.withInv 𝓘).to_pom,
-        ∃ 𝓙₂', Framed 𝓘 𝓠₂ 𝓕 𝓙₂' ν₂ := by
+        Distr.Keeps μ₂ ν₂ ∧ ∃ 𝓙₂', Framed 𝓘 𝓠₂ 𝓕 𝓙₂' ν₂ := by
     intro 𝓕 𝓙₂ μ₂ hf₂ ν₂ hν₂
-    obtain ⟨𝓠, 𝓙₂', hf', hψ⟩ := h₂ μ₂ 𝓕 𝓙₂ True.intro hf₂ ν₂ hν₂
-    exact ⟨𝓙₂', hf'.mono ((hQ₂ 𝓠).mpr hψ)⟩
+    obtain ⟨hk, 𝓠, 𝓙₂', hf', -, hψ⟩ := h₂ μ₂ 𝓕 𝓙₂ True.intro hf₂ ν₂ hν₂
+    exact ⟨hk, 𝓙₂', hf'.mono ((hQ₂ 𝓠).mpr hψ)⟩
   -- The parallel composition is handled by Lemma C.6
   rw [Cmd.withInv, Cmd.to_pom] at hν
-  obtain ⟨𝓙', hf''⟩ := lemma_C6 hf' hthread₁ hthread₂ ν hν
-  -- We still need to prove that `𝓠₁` and `𝓠₂` own disjoint variables, which requires
-  -- knowing that the footprint of a postcondition is contained in that of the precondition
-  exact ⟨𝓠₁ ⊗ 𝓠₂, 𝓙', hf'',
-    𝓠₁, 𝓠₂, sorry, le_refl _, (hQ₁ 𝓠₁).mp (le_refl _), (hQ₂ 𝓠₂).mp (le_refl _)⟩
+  obtain ⟨hk, 𝓙', hf''⟩ := lemma_C6 hf' hthread₁ hthread₂ ν hν
+  -- The least models own no more variables than the preconditions of the two threads
+  have hsub₁ : 𝓠₁.dom ⊆ 𝓟₁.dom := (ProbSpace.dom_mono ((hQ₁ _).mpr hψ₁')).trans hdom₁
+  have hsub₂ : 𝓠₂.dom ⊆ 𝓟₂.dom := (ProbSpace.dom_mono ((hQ₂ _).mpr hψ₂')).trans hdom₂
+  refine ⟨hk, 𝓠₁ ⊗ 𝓠₂, 𝓙', hf'', ?_,
+    𝓠₁, 𝓠₂, hdisj.mono hsub₁ hsub₂, le_refl _, (hQ₁ 𝓠₁).mp (le_refl _), (hQ₂ 𝓠₂).mp (le_refl _)⟩
+  exact (Set.union_subset_union hsub₁ hsub₂).trans (ProbSpace.dom_mono hle)
 
 /- STRUCTURAL RULES -/
 
@@ -154,8 +161,8 @@ variable {ι : Type} [Countable ι] {𝓘 : Inv} {F : ProbSpace → Prop} {c : C
 
 lemma wp_conseq (h : φ ⊢ ψ) : wp_base 𝓘 F c φ ⊢ wp_base 𝓘 F c ψ := by
   intro 𝓟 hc μ 𝓟fr 𝓙 hF hf ν hν
-  have ⟨𝓠, 𝓙', hf', hφ⟩ := hc μ 𝓟fr 𝓙 hF hf ν hν
-  exact ⟨𝓠, 𝓙', hf', h 𝓠 hφ⟩
+  have ⟨hk, 𝓠, 𝓙', hf', hdom, hφ⟩ := hc μ 𝓟fr 𝓙 hF hf ν hν
+  exact ⟨hk, 𝓠, 𝓙', hf', hdom, h 𝓠 hφ⟩
 
 lemma wp_split {ψ : ι → OProp} :
     (⨁[ ξ ] fun v ↦ wp_base 𝓘 F c (ψ v)) ⊢ wp_base 𝓘 F c (⨁[ ξ ] ψ) := by
@@ -176,10 +183,19 @@ lemma wp_strengthen (h : ψ.Precise) :
     wp_weak 𝓘 c ψ ⊢ wp 𝓘 c ψ := by
   sorry
 
+/-- The `Frame` rule: a frame that is independent of the program's resources is preserved. -/
 lemma wp_frame :
     φ ∗ wp 𝓘 c ψ ⊢ wp 𝓘 c iprop(φ ∗ ψ) := by
-  -- Plan: run the program with the frame `𝓕 ⊗ 𝓟₁`, and rearrange the products.
-  sorry
+  rintro 𝓟 ⟨𝓟₁, 𝓟₂, hd, hle, hφ, hwp⟩ μ 𝓕 𝓙 _ hf ν hν
+  have hf' := hf.mono hle
+  have hd₁ : Disjoint 𝓟₁.dom 𝓕.dom :=
+    hf'.disj_frame.mono_left (Set.subset_union_left : 𝓟₁.dom ⊆ 𝓟₁.dom ∪ 𝓟₂.dom)
+  -- Run the program with the frame extended by `𝓟₁`
+  obtain ⟨hk, 𝓠, 𝓙', hf'', hdom, hψ⟩ := hwp μ (𝓟₁ ⊗ 𝓕) 𝓙 True.intro (hf'.right hd) ν hν
+  have hd' : Disjoint 𝓟₁.dom 𝓠.dom :=
+    (Set.disjoint_union_right.mp hf''.disj_frame).1.symm
+  refine ⟨hk, 𝓟₁ ⊗ 𝓠, 𝓙', hf''.unright hd₁, ?_, 𝓟₁, 𝓠, hd', le_refl _, hφ, hψ⟩
+  exact (Set.union_subset_union_right _ hdom).trans (ProbSpace.dom_mono hle)
 
 /--
 **Assignment rule that preserves the value of the assigned expression.**
diff --git a/PcolIris/OProp/Laws.lean b/PcolIris/OProp/Laws.lean
index c680e83..f71647e 100644
--- a/PcolIris/OProp/Laws.lean
+++ b/PcolIris/OProp/Laws.lean
@@ -55,6 +55,69 @@ lemma state_le_product_right {p q : ProbSpace} (hdisj : Disjoint p.dom q.dom) (n
 
 end ProbSpace
 
+namespace MProp
+
+/-- The pure assertion `P` only talks about the variables `V`: it requires them to be
+allocated, and only depends on their values. -/
+def Footprint (P : MProp) (V : Set Var) : Prop :=
+  ∀ σ, P σ ↔ V ⊆ σ.dom ∧ P (σ.restrict V)
+
+namespace Footprint
+
+lemma emp : (Iris.BI.BIBase.emp : MProp).Footprint ∅ :=
+  fun _ ↦ ⟨fun _ ↦ ⟨Set.empty_subset _, trivial⟩, fun _ ↦ trivial⟩
+
+lemma var_equals_literal (x : Var) (v : Val) : ($ x == Expr.literal v).Footprint {x} := by
+  intro σ
+  rw [Expr.var_equals_literal_iff, Expr.var_equals_literal_iff,
+    Mem.restrict_apply_of_mem _ (Set.mem_singleton x)]
+  exact ⟨fun h ↦ ⟨Set.singleton_subset_iff.mpr (Mem.mem_dom_of_eq_some h), h⟩, fun h ↦ h.2⟩
+
+lemma own_var (x : Var) : (own ($ x)).Footprint {x} := by
+  intro σ
+  rw [own_var_iff, own_var_iff, Mem.restrict_apply_of_mem _ (Set.mem_singleton x)]
+  refine ⟨fun h ↦ ⟨Set.singleton_subset_iff.mpr ?_, h⟩, fun h ↦ h.2⟩
+  exact Mem.mem_dom_iff.mpr (Option.isSome_iff_ne_none.mp h)
+
+/-- An equation between an expression and a literal only talks about the variables that the
+expression reads. -/
+lemma equals_literal {e : Expr} {V : Set Var} (hmono : Expr.Mono e)
+    (hread : ∀ σ, e σ = e (σ.restrict V)) (hdef : ∀ σ, (e σ).isSome → V ⊆ σ.dom) (c : Val) :
+    (e == Expr.literal c).Footprint V := by
+  intro σ
+  rw [Expr.equals_iff hmono (Expr.literal_mono c), Expr.equals_iff hmono (Expr.literal_mono c),
+    ← hread σ]
+  exact ⟨fun h ↦ ⟨hdef σ h.1, h⟩, fun h ↦ h.2⟩
+
+lemma sep {P Q : MProp} {V W : Set Var} (hP : P.Footprint V) (hQ : Q.Footprint W)
+    (hVW : Disjoint V W) : iprop(P ∗ Q).Footprint (V ∪ W) := by
+  intro σ
+  constructor
+  · rintro ⟨σ₁, σ₂, hd, hle, h₁, h₂⟩
+    have hP' : P σ := P.upcl ((Mem.le_union_left σ₁ σ₂).trans hle) h₁
+    have hQ' : Q σ := Q.upcl ((Mem.le_union_right hd).trans hle) h₂
+    refine ⟨Set.union_subset ((hP σ).mp hP').1 ((hQ σ).mp hQ').1,
+      σ.restrict V, σ.restrict W, ?_, ?_, ((hP σ).mp hP').2, ((hQ σ).mp hQ').2⟩
+    · exact hVW.mono (Mem.dom_restrict_subset σ V) (Mem.dom_restrict_subset σ W)
+    · rw [Mem.restrict_union_restrict]
+  · rintro ⟨-, h⟩
+    exact iprop(P ∗ Q).upcl (Mem.restrict_le σ (V ∪ W)) h
+
+lemma and {P Q : MProp} {V W : Set Var} (hP : P.Footprint V) (hQ : Q.Footprint W) :
+    iprop(P ∧ Q).Footprint (V ∪ W) := by
+  intro σ
+  change P σ ∧ Q σ ↔ V ∪ W ⊆ σ.dom ∧ (P (σ.restrict (V ∪ W)) ∧ Q (σ.restrict (V ∪ W)))
+  rw [hP σ, hQ σ, hP (σ.restrict (V ∪ W)), hQ (σ.restrict (V ∪ W)), Mem.restrict_restrict,
+    Mem.restrict_restrict, Mem.restrict_dom,
+    Set.inter_eq_right.mpr (Set.subset_union_left : V ⊆ V ∪ W),
+    Set.inter_eq_right.mpr (Set.subset_union_right : W ⊆ V ∪ W)]
+  simp only [Set.union_subset_iff, Set.subset_inter_iff]
+  tauto
+
+end Footprint
+
+end MProp
+
 namespace OProp
 
 /--
@@ -83,11 +146,37 @@ lemma sure_sep_intro {P Q : MProp} : iprop(⌈P⌉ ∗ ⌈Q⌉) ⊢ ⌈ iprop(P
   · have := hg.state n hn
     rwa [ProbSpace.product_state] at this
 
-lemma sure_sep {P Q : MProp} :
-    ⌈ iprop(P ∗ Q) ⌉ ⊣⊢ ⌈P⌉ ∗ ⌈Q⌉ := by
-  constructor
-  · intro 𝓟 hsure; sorry
-  · exact sure_sep_intro
+/-- A certainty about a separating conjunction can be split into independent certainties, when
+the two assertions talk about fixed sets of variables: the two parts are the spaces without
+probabilistic information over those variables. -/
+lemma sure_sep_elim {P Q : MProp} {V W : Set Var} (hP : P.Footprint V) (hQ : Q.Footprint W) :
+    ⌈ iprop(P ∗ Q) ⌉ ⊢ iprop(⌈P⌉ ∗ ⌈Q⌉) := by
+  intro 𝓟 h
+  -- The components of a memory satisfying `P ∗ Q` satisfy `P` and `Q`
+  have hsplit : ∀ k ∈ 𝓟.support, P (𝓟.state k) ∧ Q (𝓟.state k) := by
+    intro k hk
+    obtain ⟨σ₁, σ₂, hd, hle, h₁, h₂⟩ := h hk
+    exact ⟨P.upcl ((Mem.le_union_left σ₁ σ₂).trans hle) h₁,
+      Q.upcl ((Mem.le_union_right hd).trans hle) h₂⟩
+  obtain ⟨k₀, hk₀⟩ := ProbSpace.support_nonempty 𝓟
+  obtain ⟨σ₁, σ₂, hd, hle, h₁, h₂⟩ := h hk₀
+  have hV : V ⊆ 𝓟.dom := by
+    rw [← 𝓟.dom_valid k₀]; exact ((hP _).mp (hsplit k₀ hk₀).1).1
+  have hW : W ⊆ 𝓟.dom := by
+    rw [← 𝓟.dom_valid k₀]; exact ((hQ _).mp (hsplit k₀ hk₀).2).1
+  have hVW : Disjoint V W := hd.mono ((hP _).mp h₁).1 ((hQ _).mp h₂).1
+  refine ⟨ProbSpace.forget 𝓟 V hV, ProbSpace.forget 𝓟 W hW, hVW,
+    ProbSpace.product_forget_le (ProbSpace.forget_le 𝓟 hV) hW, fun k _ ↦ ?_, fun k _ ↦ ?_⟩
+  · obtain ⟨k', hk', heq⟩ := ProbSpace.forget_state_restrict 𝓟 hV k
+    change P ((ProbSpace.forget 𝓟 V hV).state k)
+    rw [heq]; exact ((hP _).mp (hsplit k' hk').1).2
+  · obtain ⟨k', hk', heq⟩ := ProbSpace.forget_state_restrict 𝓟 hW k
+    change Q ((ProbSpace.forget 𝓟 W hW).state k)
+    rw [heq]; exact ((hQ _).mp (hsplit k' hk').2).2
+
+lemma sure_sep {P Q : MProp} {V W : Set Var} (hP : P.Footprint V) (hQ : Q.Footprint W) :
+    ⌈ iprop(P ∗ Q) ⌉ ⊣⊢ ⌈P⌉ ∗ ⌈Q⌉ :=
+  ⟨sure_sep_elim hP hQ, sure_sep_intro⟩
 
 /-- A frame can be pushed into the branches of an outcome conjunction. -/
 lemma oplus_distrib {ι : Type} [Countable ι] (ξ : PMF ι) (φ : ι → OProp) (ψ : OProp) :
@@ -100,9 +189,67 @@ lemma oplus_distrib {ι : Type} [Countable ι] (ξ : PMF ι) (φ : ι → OProp)
       ((ProbSpace.product_mono_left hsum hd).trans hle)
   · exact ⟨𝓠 v, m₂, (hdom v).symm ▸ hd.mono_left hV, le_refl _, hφ v hv, hψ⟩
 
-lemma oplus_distrib' {ι : Type} [Countable ι] (ξ : PMF ι) (φ : ι → OProp) (ψ : OProp) (h : ψ.Precise) :
-    (⨁[ ξ ] fun v ↦ iprop(φ v ∗ ψ)) ⊢ (⨁[ ξ ] φ) ∗ ψ := by
-  sorry
+/-- A precise frame can be pulled out of the branches of an outcome conjunction.  The frame
+is satisfied by the same (least) space in every branch, and the rest of each branch, completed
+by the variables it does not constrain, is independent of it. -/
+lemma oplus_distrib' {ι : Type} [Countable ι] (ξ : PMF ι) (φ : ι → OProp) (ψ : OProp)
+    (h : ψ.Precise) : (⨁[ ξ ] fun v ↦ iprop(φ v ∗ ψ)) ⊢ (⨁[ ξ ] φ) ∗ ψ := by
+  classical
+  rintro 𝓟 ⟨𝓡, W, hdsj, hdom, hsum, hφψ⟩
+  obtain ⟨v₀, hv₀⟩ := ξ.support_nonempty
+  choose m₁ m₂ hd hle h₁ h₂ using hφψ
+  obtain ⟨𝓠, hQ⟩ := h _ (h₂ v₀ hv₀)
+  have hQle : ∀ v (hv : v ∈ ξ.support), 𝓠 ≤ m₂ v hv := fun v hv ↦ (hQ _).mpr (h₂ v hv)
+  have hsubW : ∀ v (hv : v ∈ ξ.support), (m₁ v hv).dom ∪ (m₂ v hv).dom ⊆ W := fun v hv ↦ by
+    rw [← hdom v]; exact ProbSpace.dom_mono (hle v hv)
+  have hQW : 𝓠.dom ⊆ W :=
+    (ProbSpace.dom_mono (hQle v₀ hv₀)).trans (Set.subset_union_right.trans (hsubW v₀ hv₀))
+  set D := W \ 𝓠.dom with hD
+  have hm₁Q : ∀ v (hv : v ∈ ξ.support), Disjoint (m₁ v hv).dom 𝓠.dom :=
+    fun v hv ↦ (hd v hv).mono_right (ProbSpace.dom_mono (hQle v hv))
+  have hm₁D : ∀ v (hv : v ∈ ξ.support), (m₁ v hv).dom ⊆ D := fun v hv x hx ↦
+    ⟨Set.subset_union_left.trans (hsubW v hv) hx, Set.disjoint_left.mp (hm₁Q v hv) hx⟩
+  have hDR : ∀ v, D \ ∅ ⊆ (𝓡 v).dom := fun v ↦ by
+    rw [hdom v, Set.diff_empty]; exact Set.diff_subset
+  -- In each branch, the part of the space that does not belong to the frame
+  let A : ∀ v, v ∈ ξ.support → ProbSpace := fun v hv ↦
+    m₁ v hv ⊗ ProbSpace.forget (𝓡 v) (D \ (m₁ v hv).dom)
+      ((Set.diff_subset_diff_right (Set.empty_subset _)).trans (hDR v))
+  have hAdom : ∀ v hv, (A v hv).dom = D := fun v hv ↦ Set.union_diff_cancel (hm₁D v hv)
+  have hAφ : ∀ v hv, φ v (A v hv) := fun v hv ↦
+    (φ v).mono (ProbSpace.le_product_left _ _) (h₁ v hv)
+  have hAQ : ∀ v hv, (A v hv ⊗ 𝓠) ≤ 𝓡 v := by
+    intro v hv
+    have hF : Disjoint 𝓠.dom (D \ (m₁ v hv).dom) :=
+      Set.disjoint_left.mpr fun x hx hx' ↦ hx'.1.2 hx
+    refine (ProbSpace.product_swap_right hF ?_).trans ?_
+    · exact Set.disjoint_union_right.mpr ⟨hm₁Q v hv,
+        Set.disjoint_left.mpr fun x hx hx' ↦ hx'.2 hx⟩
+    · exact ProbSpace.product_forget_le
+        ((ProbSpace.product_mono_right (hQle v hv) (hm₁Q v hv)).trans (hle v hv)) _
+  let A' : ι → ProbSpace := fun v ↦ if hv : v ∈ ξ.support then A v hv else A v₀ hv₀
+  have hA'dom : ∀ v, (A' v).dom = D := fun v ↦ by
+    simp only [A']; split_ifs with hv
+    · exact hAdom v hv
+    · exact hAdom v₀ hv₀
+  obtain ⟨code, hcode⟩ := Countable.exists_injective_nat ι
+  let S : ι → ProbSpace := fun v ↦ (A' v).shift (code v)
+  have hSdisj : ∀ {i j : ι}, i ≠ j → Disjoint (S i).support (S j).support :=
+    fun hij ↦ ProbSpace.disjoint_support_shift _ _ (hcode.ne hij)
+  have hSdom : ∀ v, (S v).dom = D := hA'dom
+  refine ⟨ProbSpace.sum ξ S D hSdisj hSdom, 𝓠, Set.disjoint_sdiff_left, ?_,
+    ⟨S, D, hSdisj, hSdom, le_refl _, fun v hv ↦ ?_⟩, (hQ 𝓠).mp (le_refl _)⟩
+  · refine (ProbSpace.sum_product_le_sumProd ξ S 𝓠 D hSdisj hSdom).trans
+      ((ProbSpace.sum_mono (ProbSpace.sum_prod_disjoint 𝓠 hSdisj) hdsj
+        (ProbSpace.sum_prod_dom 𝓠 hSdom) hdom (Set.union_subset Set.diff_subset hQW)
+        fun v hv ↦ ?_).trans hsum)
+    have hv' : v ∈ ξ.support := (PMF.mem_support_iff _ _).mpr hv
+    have hA' : A' v = A v hv' := dif_pos hv'
+    refine (ProbSpace.product_mono_left (ProbSpace.shift_le _ _) ?_).trans ?_
+    · rw [hA'dom]; exact Set.disjoint_sdiff_left
+    · rw [hA']; exact hAQ v hv'
+  · have hA' : A' v = A v hv := dif_pos hv
+    exact (φ v).mono (ProbSpace.le_shift _ _) (hA' ▸ hAφ v hv)
 
 lemma oplus_weaken {ξ : PMF Val} {φ ψ : Val → OProp} (h : ∀ v ∈ ξ.support, φ v ⊢ ψ v) :
     (⨁[ξ] φ) ⊢ ⨁[ξ] ψ := by
@@ -173,54 +320,6 @@ lemma oplus_reindex {ι : Type} [Countable ι] {ξ : PMF ι} (e : ι ≃ ι) (h
 
 end OProp
 
-namespace MProp
-
-/-- The pure assertion `P` only talks about the variables `V`: it requires them to be
-allocated, and only depends on their values. -/
-def Footprint (P : MProp) (V : Set Var) : Prop :=
-  ∀ σ, P σ ↔ V ⊆ σ.dom ∧ P (σ.restrict V)
-
-namespace Footprint
-
-lemma emp : (Iris.BI.BIBase.emp : MProp).Footprint ∅ :=
-  fun _ ↦ ⟨fun _ ↦ ⟨Set.empty_subset _, trivial⟩, fun _ ↦ trivial⟩
-
-lemma var_equals_literal (x : Var) (v : Val) : ($ x == Expr.literal v).Footprint {x} := by
-  intro σ
-  rw [Expr.var_equals_literal_iff, Expr.var_equals_literal_iff,
-    Mem.restrict_apply_of_mem _ (Set.mem_singleton x)]
-  exact ⟨fun h ↦ ⟨Set.singleton_subset_iff.mpr (Mem.mem_dom_of_eq_some h), h⟩, fun h ↦ h.2⟩
-
-lemma own_var (x : Var) : (own ($ x)).Footprint {x} := by
-  intro σ
-  rw [own_var_iff, own_var_iff, Mem.restrict_apply_of_mem _ (Set.mem_singleton x)]
-  refine ⟨fun h ↦ ⟨Set.singleton_subset_iff.mpr ?_, h⟩, fun h ↦ h.2⟩
-  exact Mem.mem_dom_iff.mpr (Option.isSome_iff_ne_none.mp h)
-
-/-- An equation between an expression and a literal only talks about the variables that the
-expression reads. -/
-lemma equals_literal {e : Expr} {V : Set Var} (hmono : Expr.Mono e)
-    (hread : ∀ σ, e σ = e (σ.restrict V)) (hdef : ∀ σ, (e σ).isSome → V ⊆ σ.dom) (c : Val) :
-    (e == Expr.literal c).Footprint V := by
-  intro σ
-  rw [Expr.equals_iff hmono (Expr.literal_mono c), Expr.equals_iff hmono (Expr.literal_mono c),
-    ← hread σ]
-  exact ⟨fun h ↦ ⟨hdef σ h.1, h⟩, fun h ↦ h.2⟩
-
-lemma and {P Q : MProp} {V W : Set Var} (hP : P.Footprint V) (hQ : Q.Footprint W) :
-    iprop(P ∧ Q).Footprint (V ∪ W) := by
-  intro σ
-  change P σ ∧ Q σ ↔ V ∪ W ⊆ σ.dom ∧ (P (σ.restrict (V ∪ W)) ∧ Q (σ.restrict (V ∪ W)))
-  rw [hP σ, hQ σ, hP (σ.restrict (V ∪ W)), hQ (σ.restrict (V ∪ W)), Mem.restrict_restrict,
-    Mem.restrict_restrict, Mem.restrict_dom,
-    Set.inter_eq_right.mpr (Set.subset_union_left : V ⊆ V ∪ W),
-    Set.inter_eq_right.mpr (Set.subset_union_right : W ⊆ V ∪ W)]
-  simp only [Set.union_subset_iff, Set.subset_inter_iff]
-  tauto
-
-end Footprint
-
-end MProp
 
 namespace Precise
 
diff --git a/PcolIris/OProp/ProductLaws.lean b/PcolIris/OProp/ProductLaws.lean
index e59dc05..e262e6d 100644
--- a/PcolIris/OProp/ProductLaws.lean
+++ b/PcolIris/OProp/ProductLaws.lean
@@ -397,6 +397,13 @@ theorem product_assoc' (p q r : ProbSpace) : (p ⊗ (q ⊗ r)) ≤ ((p ⊗ q) 
       Equiv.prodAssoc_apply, id_eq, Mem.union_assoc]
     exact le_refl _
 
+/-- Swapping the two right factors of a nested product. -/
+lemma product_swap_right {a b c : ProbSpace} (hbc : Disjoint b.dom c.dom)
+    (ha : Disjoint a.dom (b.dom ∪ c.dom)) : ((a ⊗ c) ⊗ b) ≤ ((a ⊗ b) ⊗ c) :=
+  (product_assoc a c b).trans
+    ((product_mono_right (product_comm hbc) (by rwa [Set.union_comm] at ha)).trans
+      (product_assoc' a b c))
+
 /-! ### Projections and the unit -/
 
 /-- A product carries at least the information of its left factor. -/
diff --git a/PcolIris/OProp/SumLaws.lean b/PcolIris/OProp/SumLaws.lean
index 49da442..25467c1 100644
--- a/PcolIris/OProp/SumLaws.lean
+++ b/PcolIris/OProp/SumLaws.lean
@@ -170,6 +170,29 @@ theorem sum_mono {𝓟 𝓠 : ι → ProbSpace} {V W : Set Var}
     rw [sumState_of_mem hQ hn, hG v hv n hn, sumState_of_mem hP ((hg v hv).mem_support hn)]
     exact (hg v hv).state n hn
 
+/-- A sum over a point mass is (below) its summand. -/
+theorem sum_pure_le {𝓟 : ι → ProbSpace} {V : Set Var}
+    (hP : ∀ {i j : ι}, i ≠ j → Disjoint (𝓟 i).support (𝓟 j).support)
+    (hdP : ∀ i, (𝓟 i).dom = V) (i : ι) : sum (PMF.pure i) 𝓟 V hP hdP ≤ 𝓟 i := by
+  classical
+  have hmeas : ∀ E, (sumMSpace (PMF.pure i) 𝓟).MeasurableSet' E →
+      (𝓟 i).mspace.MeasurableSet' E := by
+    intro E hE
+    have h1 := hE i (by simp)
+    have hnull : (𝓟 i).meas (E \ (𝓟 i).support) = 0 :=
+      measure_mono_null (Set.diff_subset_compl _ _) (meas_compl_support _)
+    have h2 := (𝓟 i).complete.out _ hnull
+    have := @MeasurableSet.union ℕ (𝓟 i).mspace _ _ h1 h2
+    rwa [Set.inter_union_sdiff] at this
+  refine le_of_id hmeas (fun E hE ↦ ?_) (hdP i).symm.subset
+    (fun n hn ↦ le_of_eq (sumState_of_mem hP hn))
+  refine ENNReal.coe_injective ?_
+  rw [prob_coe, prob_coe]
+  change sumMeasure (PMF.pure i) 𝓟 E = _
+  rw [sumMeasure_apply _ _ hE, sumMeasureFun, tsum_eq_single i]
+  · rw [PMF.pure_apply_self, one_mul, meas_inter_support]
+  · intro j hj; rw [PMF.pure_apply_of_ne _ _ hj, zero_mul]
+
 end SumMono
 
 end ProbSpace
diff --git a/PcolIris/OProp/TrivialSpace.lean b/PcolIris/OProp/TrivialSpace.lean
index 7448461..277dbe8 100644
--- a/PcolIris/OProp/TrivialSpace.lean
+++ b/PcolIris/OProp/TrivialSpace.lean
@@ -64,6 +64,88 @@ lemma trivialOn_le {𝓠 : ProbSpace} (hdom : V ⊆ 𝓠.dom) (g : ℕ → ℕ)
     · rw [Set.preimage_empty, measure_empty, measure_empty]
     · rw [Set.preimage_univ, measure_univ, measure_univ]
 
+/-! ### Independence of spaces without probabilistic information -/
+
+/-- A space without probabilistic information is independent of every other space: if `X` is
+below `Z`, and the memories of `T` are (almost surely) restrictions of those of `Z` to other
+variables, then `X ⊗ T` is below `Z`. -/
+theorem product_trivialOn_le {X Z : ProbSpace} (hX : X ≤ Z) (hU : V ⊆ Z.dom) (t : ℕ → ℕ)
+    (ht : ∀ k ∈ Z.support, f (t k) ≤ Z.state k) : (X ⊗ trivialOn V f hf) ≤ Z := by
+  obtain ⟨g, hg⟩ := hX
+  haveI := isProbabilityMeasure_meas X
+  haveI := isProbabilityMeasure_meas (trivialOn V f hf)
+  have hgm : @Measurable ℕ ℕ Z.mspace X.mspace g := fun E hE ↦ hg.mspace E hE
+  have htm : @Measurable ℕ ℕ Z.mspace (trivialOn V f hf).mspace t := by
+    intro s hs
+    rcases trivialOn_measurableSet hs with rfl | rfl
+    · exact Z.mspace.measurableSet_empty
+    · exact @MeasurableSet.univ ℕ Z.mspace
+  have hmeas : @Measurable ℕ (ℕ × ℕ) Z.mspace (X.mspace.prod (trivialOn V f hf).mspace)
+      (fun k ↦ (g k, t k)) :=
+    @Measurable.prodMk ℕ Z.mspace ℕ ℕ X.mspace (trivialOn V f hf).mspace g t hgm htm
+  have hmap : MP Z.mspace (X.mspace.prod (trivialOn V f hf).mspace) (fun k ↦ (g k, t k))
+      Z.meas (@Measure.prod ℕ ℕ X.mspace (trivialOn V f hf).mspace X.meas
+        (trivialOn V f hf).meas) := by
+    refine @MeasurePreserving.mk ℕ (ℕ × ℕ) Z.mspace (X.mspace.prod (trivialOn V f hf).mspace)
+      _ _ _ hmeas ?_
+    symm
+    refine @ext_of_generate_finite _ (X.mspace.prod (trivialOn V f hf).mspace) _ _
+      (Set.image2 (fun x1 x2 ↦ x1 ×ˢ x2) {s | @MeasurableSet ℕ X.mspace s}
+        {t | @MeasurableSet ℕ (trivialOn V f hf).mspace t})
+      (@generateFrom_prod ℕ ℕ X.mspace (trivialOn V f hf).mspace).symm
+      (@isPiSystem_prod ℕ ℕ X.mspace (trivialOn V f hf).mspace) inferInstance ?_ ?_
+    · rintro _ ⟨A, hA, B, hB, rfl⟩
+      rw [@Measure.map_apply ℕ (ℕ × ℕ) Z.mspace (X.mspace.prod (trivialOn V f hf).mspace)
+        Z.meas _ hmeas _ (@MeasurableSet.prod ℕ ℕ X.mspace (trivialOn V f hf).mspace A B hA hB),
+        @Measure.prod_prod ℕ ℕ X.mspace (trivialOn V f hf).mspace X.meas _ _ A B]
+      rcases trivialOn_measurableSet (V := V) (f := f) (hf := hf) hB with rfl | rfl
+      · simp
+      · rw [measure_univ, mul_one, Set.mk_preimage_prod, Set.preimage_univ, Set.inter_univ]
+        exact (hg.measurePreserving.measure_preimage
+          (@MeasurableSet.nullMeasurableSet ℕ X.mspace X.meas A hA)).symm
+    · rw [@Measure.map_apply ℕ (ℕ × ℕ) Z.mspace (X.mspace.prod (trivialOn V f hf).mspace)
+        Z.meas _ hmeas _ MeasurableSet.univ, Set.preimage_univ, measure_univ, measure_univ]
+  refine ⟨fun k ↦ Nat.pairEquiv (g k, t k),
+    relabels_of_measurePreserving (IsCompletionOf.product X (trivialOn V f hf))
+      ((measurePreserving_pair X _).comp hmap) (Set.union_subset hg.dom hU) ?_⟩
+  intro k hk
+  rw [product_state, Equiv.symm_apply_apply]
+  exact Mem.union_le (hg.state k hk) (ht k hk)
+
+/-- The part of `Z` over the variables `U`, forgetting all probabilistic information: its
+memories are the (possible) memories of `Z`, restricted to `U`. -/
+noncomputable def forget (Z : ProbSpace) (U : Set Var) (hU : U ⊆ Z.dom) : ProbSpace :=
+  open Classical in
+  trivialOn U
+    (fun k ↦ (Z.state (if k ∈ Z.support then k else (support_nonempty Z).some)).restrict U)
+    (fun k ↦ by rw [Mem.restrict_dom, Z.dom_valid]; exact Set.inter_eq_right.mpr hU)
+
+lemma forget_state_restrict (Z : ProbSpace) {U : Set Var} (hU : U ⊆ Z.dom) (k : ℕ) :
+    ∃ k' ∈ Z.support, (forget Z U hU).state k = (Z.state k').restrict U := by
+  classical
+  by_cases hk : k ∈ Z.support
+  · exact ⟨k, hk, by simp only [forget, trivialOn, if_pos hk]⟩
+  · exact ⟨_, (support_nonempty Z).some_mem, by simp only [forget, trivialOn, if_neg hk]⟩
+
+lemma forget_state_of_mem (Z : ProbSpace) {U : Set Var} (hU : U ⊆ Z.dom) {k : ℕ}
+    (hk : k ∈ Z.support) : (forget Z U hU).state k = (Z.state k).restrict U := by
+  classical
+  simp only [forget, trivialOn, if_pos hk]
+
+lemma support_forget (Z : ProbSpace) {U : Set Var} (hU : U ⊆ Z.dom) :
+    (forget Z U hU).support = Set.univ := support_trivialOn
+
+lemma forget_le (Z : ProbSpace) {U : Set Var} (hU : U ⊆ Z.dom) : forget Z U hU ≤ Z :=
+  trivialOn_le hU id fun k hk ↦ by
+    change (forget Z U hU).state k ≤ _
+    rw [forget_state_of_mem Z hU hk]; exact Mem.restrict_le _ _
+
+lemma product_forget_le {X Z : ProbSpace} (hX : X ≤ Z) {U : Set Var} (hU : U ⊆ Z.dom) :
+    (X ⊗ forget Z U hU) ≤ Z :=
+  product_trivialOn_le hX hU id fun k hk ↦ by
+    change (forget Z U hU).state k ≤ _
+    rw [forget_state_of_mem Z hU hk]; exact Mem.restrict_le _ _
+
 end ProbSpace
 
 end Pcol
diff --git a/PcolIris/Semantics/Mem.lean b/PcolIris/Semantics/Mem.lean
index 878ee56..66a53b7 100644
--- a/PcolIris/Semantics/Mem.lean
+++ b/PcolIris/Semantics/Mem.lean
@@ -321,6 +321,13 @@ lemma restrict_le (σ : Mem) (X : Set Var) : σ.restrict X ≤ σ := by
   · rwa [restrict_apply_of_mem _ h] at hx
   · rw [restrict_apply_of_notMem _ h] at hx; exact absurd hx (by simp)
 
+lemma union_le {σ₁ σ₂ σ : Mem} (h₁ : σ₁ ≤ σ) (h₂ : σ₂ ≤ σ) : (σ₁ ⊎ σ₂) ≤ σ := by
+  rw [le_iff] at h₁ h₂ ⊢
+  intro x v hx
+  by_cases hs : x ∈ σ₁.dom
+  · rw [union_apply_of_mem_dom hs] at hx; exact h₁ x v hx
+  · rw [union_apply_of_notMem_dom hs] at hx; exact h₂ x v hx
+
 end Mem
 
 end Pcol