Add definition of Hoare logic semantics.

6 files changed, 2352 insertions, 0 deletions

diff --git a/src/Helium/Data/Pseudocode/Manipulate.agda b/src/Helium/Data/Pseudocode/Manipulate.agda
new file mode 100644
index 0000000..a798ad8
--- /dev/null
+++ b/src/Helium/Data/Pseudocode/Manipulate.agda
@@ -0,0 +1,1554 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Ways to modify pseudocode statements and expressions.
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --without-K #-}
+
+open import Data.Vec using (Vec)
+open import Helium.Data.Pseudocode.Core
+
+module Helium.Data.Pseudocode.Manipulate
+  {o} {Σ : Vec Type o}
+  where
+
+import Algebra.Solver.IdempotentCommutativeMonoid as ComMonoidSolver
+open import Data.Fin as Fin using (Fin; suc)
+open import Data.Fin.Patterns
+open import Data.Nat as ℕ using (ℕ; suc; _⊔_)
+import Data.Nat.Induction as ℕᵢ
+import Data.Nat.Properties as ℕₚ
+open import Data.Nat.Solver using (module +-*-Solver)
+open import Data.Product using (∃; _×_; _,_; proj₁; proj₂; <_,_>)
+open import Data.Sum using (_⊎_; inj₁; inj₂)
+import Data.Product.Relation.Binary.Lex.Strict as Lex
+open import Data.Vec as Vec using ([]; _∷_)
+import Data.Vec.Properties as Vecₚ
+open import Data.Vec.Relation.Unary.All as All using (All; []; _∷_)
+open import Data.Vec.Relation.Unary.Any using (Any; here; there)
+open import Function using (_on_; _∘_; _∋_; case_return_of_)
+open import Function.Nary.NonDependent using (congₙ)
+open import Helium.Data.Pseudocode.Properties
+import Induction.WellFounded as Wf
+import Relation.Binary.Construct.On as On
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; cong; cong₂; module ≡-Reasoning)
+open import Relation.Nullary using (yes; no; ¬_)
+open import Relation.Nullary.Decidable.Core using (True; fromWitness; toWitness; toWitnessFalse)
+open import Relation.Nullary.Negation using (contradiction)
+
+open ComMonoidSolver (record
+    { isIdempotentCommutativeMonoid = record
+      { isCommutativeMonoid = ℕₚ.⊔-0-isCommutativeMonoid
+      ; idem = ℕₚ.⊔-idem
+      }
+    })
+  using (_⊕_; _⊜_)
+  renaming (solve to ⊔-solve)
+
+open Code Σ
+
+private
+  variable
+    m n : ℕ
+    Γ Δ : Vec Type m
+    t t′ ret : Type
+
+-- TODO: make argument irrelevant
+castType : Expression Γ t → (t ≡ t′) → Expression Γ t′
+castType e refl = e
+
+cast-pres-assignable : ∀ {e : Expression Γ t} → CanAssign e → (eq : t ≡ t′) → CanAssign (castType e eq)
+cast-pres-assignable e refl = e
+
+cast-pres-stateless : ∀ {e : Expression Γ t} → (eq : t ≡ t′) → ReferencesState (castType e eq) → ReferencesState e
+cast-pres-stateless refl e = e
+
+punchOut⇒insert : ∀ {a} {A : Set a} (xs : Vec A n) {i j : Fin (suc n)} (i≢j : ¬ i ≡ j) x → Vec.lookup xs (Fin.punchOut i≢j) ≡ Vec.lookup (Vec.insert xs i x) j
+punchOut⇒insert xs {i} {j} i≢j x = begin
+  Vec.lookup xs (Fin.punchOut i≢j)
+    ≡˘⟨ cong (λ x → Vec.lookup x _) (Vecₚ.remove-insert xs i x) ⟩
+  Vec.lookup (Vec.remove (Vec.insert xs i x) i) (Fin.punchOut i≢j)
+    ≡⟨  Vecₚ.remove-punchOut (Vec.insert xs i x) i≢j ⟩
+  Vec.lookup (Vec.insert xs i x) j
+    ∎
+  where open ≡-Reasoning
+
+elimAt : ∀ i → Expression (Vec.insert Γ i t′) t  → Expression Γ t′ → Expression Γ t
+elimAt′ : ∀ i → All (Expression (Vec.insert Γ i t′)) Δ  → Expression Γ t′ → All (Expression Γ) Δ
+
+elimAt i (lit x) e′ = lit x
+elimAt i (state j) e′ = state j
+elimAt i (var j) e′ with i Fin.≟ j
+... | yes refl = castType e′ (sym (Vecₚ.insert-lookup _ i _))
+... | no i≢j = castType (var (Fin.punchOut i≢j)) (punchOut⇒insert _ i≢j _)
+elimAt i (abort e) e′ = abort (elimAt i e e′)
+elimAt i (_≟_ {hasEquality = hasEq} e e₁) e′ = _≟_ {hasEquality = hasEq} (elimAt i e e′) (elimAt i e₁ e′)
+elimAt i (_<?_ {isNumeric = isNum} e e₁) e′ = _<?_ {isNumeric = isNum} (elimAt i e e′) (elimAt i e₁ e′)
+elimAt i (inv e) e′ = elimAt i e e′
+elimAt i (e && e₁) e′ = elimAt i e e′ && elimAt i e₁ e′
+elimAt i (e || e₁) e′ = elimAt i e e′ || elimAt i e₁ e′
+elimAt i (not e) e′ = not (elimAt i e e′)
+elimAt i (e and e₁) e′ = elimAt i e e′ and elimAt i e₁ e′
+elimAt i (e or e₁) e′ = elimAt i e e′ or elimAt i e₁ e′
+elimAt i [ e ] e′ = [ elimAt i e e′ ]
+elimAt i (unbox e) e′ = unbox (elimAt i e e′)
+elimAt i (splice e e₁ e₂) e′ = splice (elimAt i e e′) (elimAt i e₁ e′) (elimAt i e₂ e′)
+elimAt i (cut e e₁) e′ = cut (elimAt i e e′) (elimAt i e₁ e′)
+elimAt i (cast eq e) e′ = cast eq (elimAt i e e′)
+elimAt i (-_ {isNumeric = isNum} e) e′ = -_ {isNumeric = isNum} (elimAt i e e′)
+elimAt i (e + e₁) e′ = elimAt i e e′ + elimAt i e₁ e′
+elimAt i (e * e₁) e′ = elimAt i e e′ * elimAt i e₁ e′
+elimAt i (_^_ {isNumeric = isNum} e x) e′ = _^_ {isNumeric = isNum} (elimAt i e e′) x
+elimAt i (e >> x) e′ = elimAt i e e′ >> x
+elimAt i (rnd e) e′ = rnd (elimAt i e e′)
+elimAt i (fin x e) e′ = fin x (elimAt i e e′)
+elimAt i (asInt e) e′ = asInt (elimAt i e e′)
+elimAt i nil e′ = nil
+elimAt i (cons e e₁) e′ = cons (elimAt i e e′) (elimAt i e₁ e′)
+elimAt i (head e) e′ = head (elimAt i e e′)
+elimAt i (tail e) e′ = tail (elimAt i e e′)
+elimAt i (call f es) e′ = call f (elimAt′ i es e′)
+elimAt i (if e then e₁ else e₂) e′ = if elimAt i e e′ then elimAt i e₁ e′ else elimAt i e₂ e′
+
+elimAt′ i []       e′ = []
+elimAt′ i (e ∷ es) e′ = elimAt i e e′ ∷ elimAt′ i es e′
+
+wknAt  : ∀ i → Expression Γ t → Expression (Vec.insert Γ i t′) t
+wknAt′ : ∀ i → All (Expression Γ) Δ  → All (Expression (Vec.insert Γ i t′)) Δ
+
+wknAt i (lit x) = lit x
+wknAt i (state j) = state j
+wknAt i (var j) = castType (var (Fin.punchIn i j)) (Vecₚ.insert-punchIn _ i _ j)
+wknAt i (abort e) = abort (wknAt i e)
+wknAt i (_≟_ {hasEquality = hasEq} e e₁) = _≟_ {hasEquality = hasEq} (wknAt i e) (wknAt i e₁)
+wknAt i (_<?_ {isNumeric = isNum} e e₁) = _<?_ {isNumeric = isNum} (wknAt i e) (wknAt i e₁)
+wknAt i (inv e) = inv (wknAt i e)
+wknAt i (e && e₁) = wknAt i e && wknAt i e₁
+wknAt i (e || e₁) = wknAt i e && wknAt i e₁
+wknAt i (not e) = not (wknAt i e)
+wknAt i (e and e₁) = wknAt i e and wknAt i e₁
+wknAt i (e or e₁) = wknAt i e or wknAt i e₁
+wknAt i [ e ] = [ wknAt i e ]
+wknAt i (unbox e) = unbox (wknAt i e)
+wknAt i (splice e e₁ e₂) = splice (wknAt i e) (wknAt i e₁) (wknAt i e₂)
+wknAt i (cut e e₁) = cut (wknAt i e) (wknAt i e₁)
+wknAt i (cast eq e) = cast eq (wknAt i e)
+wknAt i (-_ {isNumeric = isNum} e) = -_ {isNumeric = isNum} (wknAt i e)
+wknAt i (e + e₁) = wknAt i e + wknAt i e₁
+wknAt i (e * e₁) = wknAt i e * wknAt i e₁
+wknAt i (_^_ {isNumeric = isNum} e x) = _^_ {isNumeric = isNum} (wknAt i e) x
+wknAt i (e >> x) = wknAt i e >> x
+wknAt i (rnd e) = rnd (wknAt i e)
+wknAt i (fin x e) = fin x (wknAt i e)
+wknAt i (asInt e) = asInt (wknAt i e)
+wknAt i nil = nil
+wknAt i (cons e e₁) = cons (wknAt i e) (wknAt i e₁)
+wknAt i (head e) = head (wknAt i e)
+wknAt i (tail e) = tail (wknAt i e)
+wknAt i (call f es) = call f (wknAt′ i es)
+wknAt i (if e then e₁ else e₂) = if wknAt i e then wknAt i e₁ else wknAt i e₂
+
+wknAt′ i []       = []
+wknAt′ i (e ∷ es) = wknAt i e ∷ wknAt′ i es
+
+substAt : ∀ i → Expression Γ t → Expression Γ (Vec.lookup Γ i) → Expression Γ t
+substAt′ : ∀ i → All (Expression Γ) Δ → Expression Γ (Vec.lookup Γ i) → All (Expression Γ) Δ
+substAt i (lit x) e′ = lit x
+substAt i (state j) e′ = state j
+substAt i (var j) e′ with i Fin.≟ j
+... | yes refl = e′
+... | no _     = var j
+substAt i (abort e) e′ = abort (substAt i e e′)
+substAt i (_≟_ {hasEquality = hasEq} e e₁) e′ = _≟_ {hasEquality = hasEq} (substAt i e e′) (substAt i e₁ e′)
+substAt i (_<?_ {isNumeric = isNum} e e₁) e′ = _<?_ {isNumeric = isNum} (substAt i e e′) (substAt i e₁ e′)
+substAt i (inv e) e′ = inv (substAt i e e′)
+substAt i (e && e₁) e′ = substAt i e e′ && substAt i e₁ e′
+substAt i (e || e₁) e′ = substAt i e e′ || substAt i e₁ e′
+substAt i (not e) e′ = not (substAt i e e′)
+substAt i (e and e₁) e′ = substAt i e e′ and substAt i e₁ e′
+substAt i (e or e₁) e′ = substAt i e e′ or substAt i e₁ e′
+substAt i [ e ] e′ = [ substAt i e e′ ]
+substAt i (unbox e) e′ = unbox (substAt i e e′)
+substAt i (splice e e₁ e₂) e′ = splice (substAt i e e′) (substAt i e₁ e′) (substAt i e₂ e′)
+substAt i (cut e e₁) e′ = cut (substAt i e e′) (substAt i e₁ e′)
+substAt i (cast eq e) e′ = cast eq (substAt i e e′)
+substAt i (-_ {isNumeric = isNum} e) e′ = -_ {isNumeric = isNum} (substAt i e e′)
+substAt i (e + e₁) e′ = substAt i e e′ + substAt i e₁ e′
+substAt i (e * e₁) e′ = substAt i e e′ * substAt i e₁ e′
+substAt i (_^_ {isNumeric = isNum} e x) e′ = _^_ {isNumeric = isNum} (substAt i e e′) x
+substAt i (e >> x) e′ = substAt i e e′ >> x
+substAt i (rnd e) e′ = rnd (substAt i e e′)
+substAt i (fin x e) e′ = fin x (substAt i e e′)
+substAt i (asInt e) e′ = asInt (substAt i e e′)
+substAt i nil e′ = nil
+substAt i (cons e e₁) e′ = cons (substAt i e e′) (substAt i e₁ e′)
+substAt i (head e) e′ = head (substAt i e e′)
+substAt i (tail e) e′ = tail (substAt i e e′)
+substAt i (call f es) e′ = call f (substAt′ i es e′)
+substAt i (if e then e₁ else e₂) e′ = if substAt i e e′ then substAt i e₁ e′ else substAt i e₂ e′
+
+substAt′ i []       e′ = []
+substAt′ i (e ∷ es) e′ = substAt i e e′ ∷ substAt′ i es e′
+
+updateRef : ∀ {e : Expression Γ t} (ref : CanAssign e) → ¬ ReferencesState e → Expression Γ t → Expression Γ t′ → Expression Γ t′
+updateRef (state i) stateless val e = contradiction (state i) stateless
+updateRef (var i) stateless val e = substAt i e val
+updateRef (abort _) stateless val e = e
+updateRef [ ref ] stateless val e = updateRef ref (stateless ∘ [_]) (unbox val) e
+updateRef (unbox ref) stateless val e = updateRef ref (stateless ∘ unbox) [ val ] e
+updateRef (splice ref ref₁ e₂) stateless val e = updateRef ref₁ (stateless ∘ (λ x → spliceʳ _ x _)) (head (tail (cut val e₂))) (updateRef ref (stateless ∘ (λ x → spliceˡ x _ _)) (head (cut val e₂)) e)
+updateRef (cut ref e₁) stateless val e = updateRef ref (stateless ∘ (λ x → cut x _)) (splice (head val) (head (tail val)) e₁) e
+updateRef (cast eq ref) stateless val e = updateRef ref (stateless ∘ cast eq) (cast (sym eq) val) e
+updateRef nil stateless val e = e
+updateRef (cons ref ref₁) stateless val e = updateRef ref₁ (stateless ∘ (λ x → consʳ _ x)) (tail val) (updateRef ref (stateless ∘ (λ x → consˡ x _)) (head val) e)
+updateRef (head {e = e′} ref) stateless val e = updateRef ref (stateless ∘ head) (cons val (tail e′)) e
+updateRef (tail {e = e′} ref) stateless val e = updateRef ref (stateless ∘ tail) (cons (head e′) val) e
+
+wknAt-pres-assignable : ∀ i {e} → CanAssign e → CanAssign (wknAt {Γ = Γ} {t} {t′} i e)
+wknAt-pres-assignable i (state j) = state j
+wknAt-pres-assignable i (var j) = cast-pres-assignable (var (Fin.punchIn i j)) (Vecₚ.insert-punchIn _ i _ j)
+wknAt-pres-assignable i (abort e) = abort (wknAt i e)
+wknAt-pres-assignable i [ ref ] = [ wknAt-pres-assignable i ref ]
+wknAt-pres-assignable i (unbox ref) = unbox (wknAt-pres-assignable i ref)
+wknAt-pres-assignable i (splice ref ref₁ e₂) = splice (wknAt-pres-assignable i ref) (wknAt-pres-assignable i ref₁) (wknAt i e₂)
+wknAt-pres-assignable i (cut ref e₁) = cut (wknAt-pres-assignable i ref) (wknAt i e₁)
+wknAt-pres-assignable i (cast eq ref) = cast eq (wknAt-pres-assignable i ref)
+wknAt-pres-assignable i nil = nil
+wknAt-pres-assignable i (cons ref ref₁) = cons (wknAt-pres-assignable i ref) (wknAt-pres-assignable i ref₁)
+wknAt-pres-assignable i (head ref) = head (wknAt-pres-assignable i ref)
+wknAt-pres-assignable i (tail ref) = tail (wknAt-pres-assignable i ref)
+
+wknAt-pres-stateless : ∀ i {e} → ReferencesState (wknAt {Γ = Γ} {t} {t′} i e) → ReferencesState e
+wknAt-pres-stateless i {state _} (state j) = state j
+wknAt-pres-stateless i {var j} e = contradiction (cast-pres-stateless {e = var (Fin.punchIn i j)} (Vecₚ.insert-punchIn _ i _ j) e) (λ ())
+wknAt-pres-stateless i {[ _ ]} [ e ] = [ wknAt-pres-stateless i e  ]
+wknAt-pres-stateless i {unbox _} (unbox e) = unbox (wknAt-pres-stateless i e)
+wknAt-pres-stateless i {splice _ _ _} (spliceˡ e e₁ e₂) = spliceˡ (wknAt-pres-stateless i e) _ _
+wknAt-pres-stateless i {splice _ _ _} (spliceʳ e e₁ e₂) = spliceʳ _ (wknAt-pres-stateless i e₁) _
+wknAt-pres-stateless i {cut _ _} (cut e e₁) = cut (wknAt-pres-stateless i e) _
+wknAt-pres-stateless i {cast _ _} (cast eq e) = cast eq (wknAt-pres-stateless i e)
+wknAt-pres-stateless i {cons _ _} (consˡ e e₁) = consˡ (wknAt-pres-stateless i e) _
+wknAt-pres-stateless i {cons _ _} (consʳ e e₁) = consʳ _ (wknAt-pres-stateless i e₁)
+wknAt-pres-stateless i {head _} (head e) = head (wknAt-pres-stateless i e)
+wknAt-pres-stateless i {tail _} (tail e) = tail (wknAt-pres-stateless i e)
+
+wknStatementAt : ∀ t i → Statement Γ → Statement (Vec.insert Γ i t)
+wknStatementAt t i (s ∙ s₁) = wknStatementAt t i s ∙ wknStatementAt t i s₁
+wknStatementAt t i skip = skip
+wknStatementAt t i (_≔_ ref {assignable} x) = _≔_ (wknAt i ref) {fromWitness (wknAt-pres-assignable i (toWitness assignable))} (wknAt i x)
+wknStatementAt t i (declare x s) = declare (wknAt i x) (wknStatementAt t (suc i) s)
+wknStatementAt t i (invoke p es) = invoke p (wknAt′ i es)
+wknStatementAt t i (if x then s) = if wknAt i x then wknStatementAt t i s
+wknStatementAt t i (if x then s else s₁) = if wknAt i x then wknStatementAt t i s else wknStatementAt t i s₁
+wknStatementAt t i (for m s) = for m (wknStatementAt t (suc i) s)
+
+subst : Expression Γ t → All (Expression Δ) Γ → Expression Δ t
+subst′ : ∀ {n ts} → All (Expression Γ) {n} ts → All (Expression Δ) Γ → All (Expression Δ) ts
+
+subst (lit x) xs = lit x
+subst (state i) xs = state i
+subst (var i) xs = All.lookup i xs
+subst (abort e) xs = abort (subst e xs)
+subst (_≟_ {hasEquality = hasEq} e e₁) xs = _≟_ {hasEquality = hasEq} (subst e xs) (subst e₁ xs)
+subst (_<?_ {isNumeric = isNum} e e₁) xs = _<?_ {isNumeric = isNum} (subst e xs) (subst e₁ xs)
+subst (inv e) xs = inv (subst e xs)
+subst (e && e₁) xs = subst e xs && subst e₁ xs
+subst (e || e₁) xs = subst e xs || subst e₁ xs
+subst (not e) xs = not (subst e xs)
+subst (e and e₁) xs = subst e xs and subst e₁ xs
+subst (e or e₁) xs = subst e xs or subst e₁ xs
+subst [ e ] xs = [ subst e xs ]
+subst (unbox e) xs = unbox (subst e xs)
+subst (splice e e₁ e₂) xs = splice (subst e xs) (subst e₁ xs) (subst e₂ xs)
+subst (cut e e₁) xs = cut (subst e xs) (subst e₁ xs)
+subst (cast eq e) xs = cast eq (subst e xs)
+subst (-_ {isNumeric = isNum} e) xs = -_ {isNumeric = isNum} (subst e xs)
+subst (e + e₁) xs = subst e xs + subst e₁ xs
+subst (e * e₁) xs = subst e xs * subst e₁ xs
+subst (_^_ {isNumeric = isNum} e x) xs = _^_ {isNumeric = isNum} (subst e xs) x
+subst (e >> x) xs = subst e xs >> x
+subst (rnd e) xs = rnd (subst e xs)
+subst (fin x e) xs = fin x (subst e xs)
+subst (asInt e) xs = asInt (subst e xs)
+subst nil xs = nil
+subst (cons e e₁) xs = cons (subst e xs) (subst e₁ xs)
+subst (head e) xs = head (subst e xs)
+subst (tail e) xs = tail (subst e xs)
+subst (call f es) xs = call f (subst′ es xs)
+subst (if e then e₁ else e₂) xs = if subst e xs then subst e₁ xs else subst e₂ xs
+
+subst′ []       xs = []
+subst′ (e ∷ es) xs = subst e xs ∷ subst′ es xs
+
+callDepth     : Expression Γ t → ℕ
+callDepth′  : All (Expression Γ) Δ → ℕ
+stmtCallDepth : Statement Γ → ℕ
+funCallDepth  : Function Γ ret → ℕ
+procCallDepth : Procedure Γ → ℕ
+
+callDepth (lit x) = 0
+callDepth (state i) = 0
+callDepth (var i) = 0
+callDepth (abort e) = callDepth e
+callDepth (e ≟ e₁) = callDepth e ⊔ callDepth e₁
+callDepth (e <? e₁) = callDepth e ⊔ callDepth e₁
+callDepth (inv e) = callDepth e
+callDepth (e && e₁) = callDepth e ⊔ callDepth e₁
+callDepth (e || e₁) = callDepth e ⊔ callDepth e₁
+callDepth (not e) = callDepth e
+callDepth (e and e₁) = callDepth e ⊔ callDepth e₁
+callDepth (e or e₁) = callDepth e ⊔ callDepth e₁
+callDepth [ e ] = callDepth e
+callDepth (unbox e) = callDepth e
+callDepth (splice e e₁ e₂) = callDepth e ⊔ callDepth e₁ ⊔ callDepth e₂
+callDepth (cut e e₁) = callDepth e ⊔ callDepth e₁
+callDepth (cast eq e) = callDepth e
+callDepth (- e) = callDepth e
+callDepth (e + e₁) = callDepth e ⊔ callDepth e₁
+callDepth (e * e₁) = callDepth e ⊔ callDepth e₁
+callDepth (e ^ x) = callDepth e
+callDepth (e >> x) = callDepth e
+callDepth (rnd e) = callDepth e
+callDepth (fin x e) = callDepth e
+callDepth (asInt e) = callDepth e
+callDepth nil = 0
+callDepth (cons e e₁) = callDepth e ⊔ callDepth e₁
+callDepth (head e) = callDepth e
+callDepth (tail e) = callDepth e
+callDepth (call f es) = suc (funCallDepth f) ⊔ callDepth′ es
+callDepth (if e then e₁ else e₂) = callDepth e ⊔ callDepth e₁ ⊔ callDepth e₂
+
+callDepth′ [] = 0
+callDepth′ (e ∷ es) = callDepth e ⊔ callDepth′ es
+
+stmtCallDepth (s ∙ s₁) = stmtCallDepth s ⊔ stmtCallDepth s₁
+stmtCallDepth skip = 0
+stmtCallDepth (ref ≔ x) = callDepth ref ⊔ callDepth x
+stmtCallDepth (declare x s) = callDepth x ⊔ stmtCallDepth s
+stmtCallDepth (invoke p es) = procCallDepth p ⊔ callDepth′ es
+stmtCallDepth (if x then s) = callDepth x ⊔ stmtCallDepth s
+stmtCallDepth (if x then s else s₁) = callDepth x ⊔ stmtCallDepth s ⊔ stmtCallDepth s₁
+stmtCallDepth (for m s) = stmtCallDepth s
+
+funCallDepth (s ∙return x) = stmtCallDepth s ⊔ callDepth x
+funCallDepth (declare x f) = funCallDepth f ⊔ callDepth x
+
+procCallDepth (x ∙end) = stmtCallDepth x
+
+open ℕₚ.≤-Reasoning
+
+castType-pres-callDepth : ∀ (e : Expression Γ t) (eq : t ≡ t′) → callDepth (castType e eq) ≡ callDepth e
+castType-pres-callDepth e refl = refl
+
+elimAt-pres-callDepth : ∀ i (e : Expression (Vec.insert Γ i t′) t) (e′ : Expression Γ t′) → callDepth (elimAt i e e′) ℕ.≤ callDepth e′ ⊔ callDepth e
+elimAt′-pres-callDepth : ∀ i (es : All (Expression (Vec.insert Γ i t′)) Δ) (e′ : Expression Γ t′) → callDepth′ (elimAt′ i es e′) ℕ.≤ callDepth e′ ⊔ callDepth′ es
+
+elimAt-pres-callDepth i (lit x) e′ = ℕₚ.m≤n⊔m (callDepth e′) 0
+elimAt-pres-callDepth i (state j) e′ = ℕₚ.m≤n⊔m (callDepth e′) 0
+elimAt-pres-callDepth i (var j) e′ with i Fin.≟ j
+... | yes refl = begin
+  callDepth (castType e′ (sym (Vecₚ.insert-lookup _ i _)))
+    ≡⟨ castType-pres-callDepth e′ (sym (Vecₚ.insert-lookup _ i _)) ⟩
+  callDepth e′
+    ≤⟨ ℕₚ.m≤m⊔n (callDepth e′) 0 ⟩
+  callDepth e′ ⊔ 0
+    ∎
+elimAt-pres-callDepth {Γ = Γ} i (var j) e′ | no i≢j   = begin
+    callDepth (castType (var {Γ = Γ} (Fin.punchOut i≢j)) (punchOut⇒insert Γ i≢j _))
+      ≡⟨ castType-pres-callDepth (var {Γ = Γ} (Fin.punchOut i≢j)) (punchOut⇒insert Γ i≢j _) ⟩
+    0
+      ≤⟨ ℕ.z≤n ⟩
+    callDepth e′ ⊔ 0
+      ∎
+elimAt-pres-callDepth i (abort e) e′ = elimAt-pres-callDepth i e e′
+elimAt-pres-callDepth i (e ≟ e₁) e′ = begin
+  callDepth (elimAt i e e′) ⊔ callDepth (elimAt i e₁ e′)
+    ≤⟨ ℕₚ.⊔-mono-≤ (elimAt-pres-callDepth i e e′) (elimAt-pres-callDepth i e₁ e′) ⟩
+  callDepth e′ ⊔ callDepth e ⊔ (callDepth e′ ⊔ callDepth e₁)
+    ≡⟨ ⊔-solve 3 (λ m n o → (m ⊕ n) ⊕ (m ⊕ o) ⊜ m ⊕ (n ⊕ o)) refl (callDepth e′) (callDepth e) (callDepth e₁) ⟩
+  callDepth e′ ⊔ (callDepth e ⊔ callDepth e₁)
+    ∎
+elimAt-pres-callDepth i (e <? e₁) e′ = begin
+  callDepth (elimAt i e e′) ⊔ callDepth (elimAt i e₁ e′)
+    ≤⟨ ℕₚ.⊔-mono-≤ (elimAt-pres-callDepth i e e′) (elimAt-pres-callDepth i e₁ e′) ⟩
+  callDepth e′ ⊔ callDepth e ⊔ (callDepth e′ ⊔ callDepth e₁)
+    ≡⟨ ⊔-solve 3 (λ m n o → (m ⊕ n) ⊕ (m ⊕ o) ⊜ m ⊕ (n ⊕ o)) refl (callDepth e′) (callDepth e) (callDepth e₁) ⟩
+  callDepth e′ ⊔ (callDepth e ⊔ callDepth e₁)
+    ∎
+elimAt-pres-callDepth i (inv e) e′ = elimAt-pres-callDepth i e e′
+elimAt-pres-callDepth i (e && e₁) e′ = begin
+  callDepth (elimAt i e e′) ⊔ callDepth (elimAt i e₁ e′)
+    ≤⟨ ℕₚ.⊔-mono-≤ (elimAt-pres-callDepth i e e′) (elimAt-pres-callDepth i e₁ e′) ⟩
+  callDepth e′ ⊔ callDepth e ⊔ (callDepth e′ ⊔ callDepth e₁)
+    ≡⟨ ⊔-solve 3 (λ m n o → (m ⊕ n) ⊕ (m ⊕ o) ⊜ m ⊕ (n ⊕ o)) refl (callDepth e′) (callDepth e) (callDepth e₁) ⟩
+  callDepth e′ ⊔ (callDepth e ⊔ callDepth e₁)
+    ∎
+elimAt-pres-callDepth i (e || e₁) e′ = begin
+  callDepth (elimAt i e e′) ⊔ callDepth (elimAt i e₁ e′)
+    ≤⟨ ℕₚ.⊔-mono-≤ (elimAt-pres-callDepth i e e′) (elimAt-pres-callDepth i e₁ e′) ⟩
+  callDepth e′ ⊔ callDepth e ⊔ (callDepth e′ ⊔ callDepth e₁)
+    ≡⟨ ⊔-solve 3 (λ m n o → (m ⊕ n) ⊕ (m ⊕ o) ⊜ m ⊕ (n ⊕ o)) refl (callDepth e′) (callDepth e) (callDepth e₁) ⟩
+  callDepth e′ ⊔ (callDepth e ⊔ callDepth e₁)
+    ∎
+elimAt-pres-callDepth i (not e) e′ = elimAt-pres-callDepth i e e′
+elimAt-pres-callDepth i (e and e₁) e′ = begin
+  callDepth (elimAt i e e′) ⊔ callDepth (elimAt i e₁ e′)
+    ≤⟨ ℕₚ.⊔-mono-≤ (elimAt-pres-callDepth i e e′) (elimAt-pres-callDepth i e₁ e′) ⟩
+  callDepth e′ ⊔ callDepth e ⊔ (callDepth e′ ⊔ callDepth e₁)
+    ≡⟨ ⊔-solve 3 (λ m n o → (m ⊕ n) ⊕ (m ⊕ o) ⊜ m ⊕ (n ⊕ o)) refl (callDepth e′) (callDepth e) (callDepth e₁) ⟩
+  callDepth e′ ⊔ (callDepth e ⊔ callDepth e₁)
+    ∎
+elimAt-pres-callDepth i (e or e₁) e′ = begin
+  callDepth (elimAt i e e′) ⊔ callDepth (elimAt i e₁ e′)
+    ≤⟨ ℕₚ.⊔-mono-≤ (elimAt-pres-callDepth i e e′) (elimAt-pres-callDepth i e₁ e′) ⟩
+  callDepth e′ ⊔ callDepth e ⊔ (callDepth e′ ⊔ callDepth e₁)
+    ≡⟨ ⊔-solve 3 (λ m n o → (m ⊕ n) ⊕ (m ⊕ o) ⊜ m ⊕ (n ⊕ o)) refl (callDepth e′) (callDepth e) (callDepth e₁) ⟩
+  callDepth e′ ⊔ (callDepth e ⊔ callDepth e₁)
+    ∎
+elimAt-pres-callDepth i [ e ] e′ = elimAt-pres-callDepth i e e′
+elimAt-pres-callDepth i (unbox e) e′ = elimAt-pres-callDepth i e e′
+elimAt-pres-callDepth i (splice e e₁ e₂) e′ = begin
+  callDepth (elimAt i e e′) ⊔ callDepth (elimAt i e₁ e′) ⊔ callDepth (elimAt i e₂ e′)
+    ≤⟨ ℕₚ.⊔-mono-≤ (ℕₚ.⊔-mono-≤ (elimAt-pres-callDepth i e e′) (elimAt-pres-callDepth i e₁ e′)) (elimAt-pres-callDepth i e₂ e′) ⟩
+  callDepth e′ ⊔ callDepth e ⊔ (callDepth e′ ⊔ callDepth e₁) ⊔ (callDepth e′ ⊔ callDepth e₂)
+    ≡⟨ ⊔-solve 4 (λ m n o p → (((m ⊕ n) ⊕ (m ⊕ o)) ⊕ (m ⊕ p)) ⊜ (m ⊕ ((n ⊕ o) ⊕ p))) refl (callDepth e′) (callDepth e) (callDepth e₁) (callDepth e₂) ⟩
+  callDepth e′ ⊔ (callDepth e ⊔ callDepth e₁ ⊔ callDepth e₂)
+    ∎
+elimAt-pres-callDepth i (cut e e₁) e′ = begin
+  callDepth (elimAt i e e′) ⊔ callDepth (elimAt i e₁ e′)
+    ≤⟨ ℕₚ.⊔-mono-≤ (elimAt-pres-callDepth i e e′) (elimAt-pres-callDepth i e₁ e′) ⟩
+  callDepth e′ ⊔ callDepth e ⊔ (callDepth e′ ⊔ callDepth e₁)
+    ≡⟨ ⊔-solve 3 (λ m n o → (m ⊕ n) ⊕ (m ⊕ o) ⊜ m ⊕ (n ⊕ o)) refl (callDepth e′) (callDepth e) (callDepth e₁) ⟩
+  callDepth e′ ⊔ (callDepth e ⊔ callDepth e₁)
+    ∎
+elimAt-pres-callDepth i (cast eq e) e′ = elimAt-pres-callDepth i e e′
+elimAt-pres-callDepth i (- e) e′ = elimAt-pres-callDepth i e e′
+elimAt-pres-callDepth i (e + e₁) e′ = begin
+  callDepth (elimAt i e e′) ⊔ callDepth (elimAt i e₁ e′)
+    ≤⟨ ℕₚ.⊔-mono-≤ (elimAt-pres-callDepth i e e′) (elimAt-pres-callDepth i e₁ e′) ⟩
+  callDepth e′ ⊔ callDepth e ⊔ (callDepth e′ ⊔ callDepth e₁)
+    ≡⟨ ⊔-solve 3 (λ m n o → (m ⊕ n) ⊕ (m ⊕ o) ⊜ m ⊕ (n ⊕ o)) refl (callDepth e′) (callDepth e) (callDepth e₁) ⟩
+  callDepth e′ ⊔ (callDepth e ⊔ callDepth e₁)
+    ∎
+elimAt-pres-callDepth i (e * e₁) e′ = begin
+  callDepth (elimAt i e e′) ⊔ callDepth (elimAt i e₁ e′)
+    ≤⟨ ℕₚ.⊔-mono-≤ (elimAt-pres-callDepth i e e′) (elimAt-pres-callDepth i e₁ e′) ⟩
+  callDepth e′ ⊔ callDepth e ⊔ (callDepth e′ ⊔ callDepth e₁)
+    ≡⟨ ⊔-solve 3 (λ m n o → (m ⊕ n) ⊕ (m ⊕ o) ⊜ m ⊕ (n ⊕ o)) refl (callDepth e′) (callDepth e) (callDepth e₁) ⟩
+  callDepth e′ ⊔ (callDepth e ⊔ callDepth e₁)
+    ∎
+elimAt-pres-callDepth i (e ^ x) e′ = elimAt-pres-callDepth i e e′
+elimAt-pres-callDepth i (e >> x) e′ = elimAt-pres-callDepth i e e′
+elimAt-pres-callDepth i (rnd e) e′ = elimAt-pres-callDepth i e e′
+elimAt-pres-callDepth i (fin x e) e′ = elimAt-pres-callDepth i e e′
+elimAt-pres-callDepth i (asInt e) e′ = elimAt-pres-callDepth i e e′
+elimAt-pres-callDepth i nil e′ = ℕₚ.m≤n⊔m (callDepth e′) 0
+elimAt-pres-callDepth i (cons e e₁) e′ = begin
+  callDepth (elimAt i e e′) ⊔ callDepth (elimAt i e₁ e′)
+    ≤⟨ ℕₚ.⊔-mono-≤ (elimAt-pres-callDepth i e e′) (elimAt-pres-callDepth i e₁ e′) ⟩
+  callDepth e′ ⊔ callDepth e ⊔ (callDepth e′ ⊔ callDepth e₁)
+    ≡⟨ ⊔-solve 3 (λ m n o → (m ⊕ n) ⊕ (m ⊕ o) ⊜ m ⊕ (n ⊕ o)) refl (callDepth e′) (callDepth e) (callDepth e₁) ⟩
+  callDepth e′ ⊔ (callDepth e ⊔ callDepth e₁)
+    ∎
+elimAt-pres-callDepth i (head e) e′ = elimAt-pres-callDepth i e e′
+elimAt-pres-callDepth i (tail e) e′ = elimAt-pres-callDepth i e e′
+elimAt-pres-callDepth i (call f es) e′ = begin
+  suc (funCallDepth f) ⊔ callDepth′ (elimAt′ i es e′)
+    ≤⟨ ℕₚ.⊔-monoʳ-≤ (suc (funCallDepth f)) (elimAt′-pres-callDepth i es e′) ⟩
+  suc (funCallDepth f) ⊔ (callDepth e′ ⊔ callDepth′ es)
+    ≡⟨ ⊔-solve 3 (λ a b c → b ⊕ (a ⊕ c) ⊜ a ⊕ (b ⊕ c)) refl (callDepth e′) (suc (funCallDepth f)) (callDepth′ es) ⟩
+  callDepth e′ ⊔ (suc (funCallDepth f) ⊔ callDepth′ es)
+    ∎
+elimAt-pres-callDepth i (if e then e₁ else e₂) e′ = begin
+  callDepth (elimAt i e e′) ⊔ callDepth (elimAt i e₁ e′) ⊔ callDepth (elimAt i e₂ e′)
+    ≤⟨ ℕₚ.⊔-mono-≤ (ℕₚ.⊔-mono-≤ (elimAt-pres-callDepth i e e′) (elimAt-pres-callDepth i e₁ e′)) (elimAt-pres-callDepth i e₂ e′) ⟩
+  callDepth e′ ⊔ callDepth e ⊔ (callDepth e′ ⊔ callDepth e₁) ⊔ (callDepth e′ ⊔ callDepth e₂)
+    ≡⟨ ⊔-solve 4 (λ m n o p → (((m ⊕ n) ⊕ (m ⊕ o)) ⊕ (m ⊕ p)) ⊜ (m ⊕ ((n ⊕ o) ⊕ p))) refl (callDepth e′) (callDepth e) (callDepth e₁) (callDepth e₂) ⟩
+  callDepth e′ ⊔ (callDepth e ⊔ callDepth e₁ ⊔ callDepth e₂)
+    ∎
+
+elimAt′-pres-callDepth i []       e′ = ℕₚ.m≤n⊔m (callDepth e′) 0
+elimAt′-pres-callDepth i (e ∷ es) e′ = begin
+  callDepth (elimAt i e e′) ⊔ callDepth′ (elimAt′ i es e′)
+    ≤⟨ ℕₚ.⊔-mono-≤ (elimAt-pres-callDepth i e e′) (elimAt′-pres-callDepth i es e′) ⟩
+  callDepth e′ ⊔ callDepth e ⊔ (callDepth e′ ⊔ callDepth′ es)
+    ≡⟨ ⊔-solve 3 (λ a b c → ((a ⊕ b) ⊕ (a ⊕ c)) ⊜ (a ⊕ (b ⊕ c))) refl (callDepth e′) (callDepth e) (callDepth′ es) ⟩
+  callDepth e′ ⊔ (callDepth e ⊔ callDepth′ es)
+    ∎
+
+wknAt-pres-callDepth : ∀ i (e : Expression Γ t) → callDepth (wknAt {t′ = t′} i e) ≡ callDepth e
+wknAt′-pres-callDepth : ∀ i (es : All (Expression Γ) Δ) → callDepth′ (wknAt′ {t′ = t′} i es) ≡ callDepth′ es
+
+wknAt-pres-callDepth i (Code.lit x) = refl
+wknAt-pres-callDepth i (Code.state j) = refl
+wknAt-pres-callDepth {Γ = Γ} i (Code.var j) = castType-pres-callDepth (var {Γ = Vec.insert Γ i _} (Fin.punchIn i j)) (Vecₚ.insert-punchIn Γ i _ j)
+wknAt-pres-callDepth i (Code.abort e) = wknAt-pres-callDepth i e
+wknAt-pres-callDepth i (e Code.≟ e₁) = cong₂ _⊔_ (wknAt-pres-callDepth i e) (wknAt-pres-callDepth i e₁)
+wknAt-pres-callDepth i (e Code.<? e₁) = cong₂ _⊔_ (wknAt-pres-callDepth i e) (wknAt-pres-callDepth i e₁)
+wknAt-pres-callDepth i (Code.inv e) = wknAt-pres-callDepth i e
+wknAt-pres-callDepth i (e Code.&& e₁) = cong₂ _⊔_ (wknAt-pres-callDepth i e) (wknAt-pres-callDepth i e₁)
+wknAt-pres-callDepth i (e Code.|| e₁) = cong₂ _⊔_ (wknAt-pres-callDepth i e) (wknAt-pres-callDepth i e₁)
+wknAt-pres-callDepth i (Code.not e) = wknAt-pres-callDepth i e
+wknAt-pres-callDepth i (e Code.and e₁) = cong₂ _⊔_ (wknAt-pres-callDepth i e) (wknAt-pres-callDepth i e₁)
+wknAt-pres-callDepth i (e Code.or e₁) = cong₂ _⊔_ (wknAt-pres-callDepth i e) (wknAt-pres-callDepth i e₁)
+wknAt-pres-callDepth i Code.[ e ] = wknAt-pres-callDepth i e
+wknAt-pres-callDepth i (Code.unbox e) = wknAt-pres-callDepth i e
+wknAt-pres-callDepth i (Code.splice e e₁ e₂) = congₙ 3 (λ m n o → m ⊔ n ⊔ o) (wknAt-pres-callDepth i e) (wknAt-pres-callDepth i e₁) (wknAt-pres-callDepth i e₂)
+wknAt-pres-callDepth i (Code.cut e e₁) = cong₂ _⊔_ (wknAt-pres-callDepth i e) (wknAt-pres-callDepth i e₁)
+wknAt-pres-callDepth i (Code.cast eq e) = wknAt-pres-callDepth i e
+wknAt-pres-callDepth i (Code.- e) = wknAt-pres-callDepth i e
+wknAt-pres-callDepth i (e Code.+ e₁) = cong₂ _⊔_ (wknAt-pres-callDepth i e) (wknAt-pres-callDepth i e₁)
+wknAt-pres-callDepth i (e Code.* e₁) = cong₂ _⊔_ (wknAt-pres-callDepth i e) (wknAt-pres-callDepth i e₁)
+wknAt-pres-callDepth i (e Code.^ x) = wknAt-pres-callDepth i e
+wknAt-pres-callDepth i (e Code.>> x) = wknAt-pres-callDepth i e
+wknAt-pres-callDepth i (Code.rnd e) = wknAt-pres-callDepth i e
+wknAt-pres-callDepth i (Code.fin x e) = wknAt-pres-callDepth i e
+wknAt-pres-callDepth i (Code.asInt e) = wknAt-pres-callDepth i e
+wknAt-pres-callDepth i Code.nil = refl
+wknAt-pres-callDepth i (Code.cons e e₁) = cong₂ _⊔_ (wknAt-pres-callDepth i e) (wknAt-pres-callDepth i e₁)
+wknAt-pres-callDepth i (Code.head e) = wknAt-pres-callDepth i e
+wknAt-pres-callDepth i (Code.tail e) = wknAt-pres-callDepth i e
+wknAt-pres-callDepth i (Code.call f es) = cong (suc (funCallDepth f) ⊔_) (wknAt′-pres-callDepth i es)
+wknAt-pres-callDepth i (Code.if e then e₁ else e₂) = congₙ 3 (λ m n o → m ⊔ n ⊔ o) (wknAt-pres-callDepth i e) (wknAt-pres-callDepth i e₁) (wknAt-pres-callDepth i e₂)
+
+wknAt′-pres-callDepth i []       = refl
+wknAt′-pres-callDepth i (e ∷ es) = cong₂ _⊔_ (wknAt-pres-callDepth i e) (wknAt′-pres-callDepth i es)
+
+substAt-pres-callDepth : ∀ i (e : Expression Γ t) e′ → callDepth (substAt i e e′) ℕ.≤ callDepth e′ ⊔ callDepth e
+substAt-pres-callDepth i (Code.lit x) e′ = ℕₚ.m≤n⊔m (callDepth e′) 0
+substAt-pres-callDepth i (Code.state j) e′ = ℕₚ.m≤n⊔m (callDepth e′) 0
+substAt-pres-callDepth i (Code.var j) e′ with i Fin.≟ j
+... | yes refl = ℕₚ.m≤m⊔n (callDepth e′) 0
+... | no _     = ℕₚ.m≤n⊔m (callDepth e′) 0
+substAt-pres-callDepth i (Code.abort e) e′ = substAt-pres-callDepth i e e′
+substAt-pres-callDepth i (e Code.≟ e₁) e′ = begin
+  callDepth (substAt i e e′) ⊔ callDepth (substAt i e₁ e′)
+    ≤⟨ ℕₚ.⊔-mono-≤ (substAt-pres-callDepth i e e′) (substAt-pres-callDepth i e₁ e′) ⟩
+  callDepth e′ ⊔ callDepth e ⊔ (callDepth e′ ⊔ callDepth e₁)
+    ≡⟨ ⊔-solve 3 (λ a b c → (a ⊕ b) ⊕ (a ⊕ c) ⊜ a ⊕ (b ⊕ c)) refl (callDepth e′) (callDepth e) (callDepth e₁) ⟩
+  callDepth e′ ⊔ (callDepth e ⊔ callDepth e₁)
+    ∎
+substAt-pres-callDepth i (e Code.<? e₁) e′ = begin
+  callDepth (substAt i e e′) ⊔ callDepth (substAt i e₁ e′)
+    ≤⟨ ℕₚ.⊔-mono-≤ (substAt-pres-callDepth i e e′) (substAt-pres-callDepth i e₁ e′) ⟩
+  callDepth e′ ⊔ callDepth e ⊔ (callDepth e′ ⊔ callDepth e₁)
+    ≡⟨ ⊔-solve 3 (λ a b c → (a ⊕ b) ⊕ (a ⊕ c) ⊜ a ⊕ (b ⊕ c)) refl (callDepth e′) (callDepth e) (callDepth e₁) ⟩
+  callDepth e′ ⊔ (callDepth e ⊔ callDepth e₁)
+    ∎
+substAt-pres-callDepth i (Code.inv e) e′ = substAt-pres-callDepth i e e′
+substAt-pres-callDepth i (e Code.&& e₁) e′ = begin
+  callDepth (substAt i e e′) ⊔ callDepth (substAt i e₁ e′)
+    ≤⟨ ℕₚ.⊔-mono-≤ (substAt-pres-callDepth i e e′) (substAt-pres-callDepth i e₁ e′) ⟩
+  callDepth e′ ⊔ callDepth e ⊔ (callDepth e′ ⊔ callDepth e₁)
+    ≡⟨ ⊔-solve 3 (λ a b c → (a ⊕ b) ⊕ (a ⊕ c) ⊜ a ⊕ (b ⊕ c)) refl (callDepth e′) (callDepth e) (callDepth e₁) ⟩
+  callDepth e′ ⊔ (callDepth e ⊔ callDepth e₁)
+    ∎
+substAt-pres-callDepth i (e Code.|| e₁) e′ = begin
+  callDepth (substAt i e e′) ⊔ callDepth (substAt i e₁ e′)
+    ≤⟨ ℕₚ.⊔-mono-≤ (substAt-pres-callDepth i e e′) (substAt-pres-callDepth i e₁ e′) ⟩
+  callDepth e′ ⊔ callDepth e ⊔ (callDepth e′ ⊔ callDepth e₁)
+    ≡⟨ ⊔-solve 3 (λ a b c → (a ⊕ b) ⊕ (a ⊕ c) ⊜ a ⊕ (b ⊕ c)) refl (callDepth e′) (callDepth e) (callDepth e₁) ⟩
+  callDepth e′ ⊔ (callDepth e ⊔ callDepth e₁)
+    ∎
+substAt-pres-callDepth i (Code.not e) e′ = substAt-pres-callDepth i e e′
+substAt-pres-callDepth i (e Code.and e₁) e′ = begin
+  callDepth (substAt i e e′) ⊔ callDepth (substAt i e₁ e′)
+    ≤⟨ ℕₚ.⊔-mono-≤ (substAt-pres-callDepth i e e′) (substAt-pres-callDepth i e₁ e′) ⟩
+  callDepth e′ ⊔ callDepth e ⊔ (callDepth e′ ⊔ callDepth e₁)
+    ≡⟨ ⊔-solve 3 (λ a b c → (a ⊕ b) ⊕ (a ⊕ c) ⊜ a ⊕ (b ⊕ c)) refl (callDepth e′) (callDepth e) (callDepth e₁) ⟩
+  callDepth e′ ⊔ (callDepth e ⊔ callDepth e₁)
+    ∎
+substAt-pres-callDepth i (e Code.or e₁) e′ = begin
+  callDepth (substAt i e e′) ⊔ callDepth (substAt i e₁ e′)
+    ≤⟨ ℕₚ.⊔-mono-≤ (substAt-pres-callDepth i e e′) (substAt-pres-callDepth i e₁ e′) ⟩
+  callDepth e′ ⊔ callDepth e ⊔ (callDepth e′ ⊔ callDepth e₁)
+    ≡⟨ ⊔-solve 3 (λ a b c → (a ⊕ b) ⊕ (a ⊕ c) ⊜ a ⊕ (b ⊕ c)) refl (callDepth e′) (callDepth e) (callDepth e₁) ⟩
+  callDepth e′ ⊔ (callDepth e ⊔ callDepth e₁)
+    ∎
+substAt-pres-callDepth i Code.[ e ] e′ = substAt-pres-callDepth i e e′
+substAt-pres-callDepth i (Code.unbox e) e′ = substAt-pres-callDepth i e e′
+substAt-pres-callDepth i (Code.splice e e₁ e₂) e′ = begin
+  callDepth (substAt i e e′) ⊔ callDepth (substAt i e₁ e′) ⊔ callDepth (substAt i e₂ e′)
+    ≤⟨ ℕₚ.⊔-mono-≤ (ℕₚ.⊔-mono-≤ (substAt-pres-callDepth i e e′) (substAt-pres-callDepth i e₁ e′)) (substAt-pres-callDepth i e₂ e′) ⟩
+  callDepth e′ ⊔ callDepth e ⊔ (callDepth e′ ⊔ callDepth e₁) ⊔ (callDepth e′ ⊔ callDepth e₂)
+    ≡⟨ ⊔-solve 4 (λ a b c d → ((a ⊕ b) ⊕ (a ⊕ c)) ⊕ (a ⊕ d) ⊜ a ⊕ ((b ⊕ c) ⊕ d)) refl (callDepth e′) (callDepth e) (callDepth e₁) (callDepth e₂) ⟩
+  callDepth e′ ⊔ (callDepth e ⊔ callDepth e₁ ⊔ callDepth e₂)
+    ∎
+substAt-pres-callDepth i (Code.cut e e₁) e′ = begin
+  callDepth (substAt i e e′) ⊔ callDepth (substAt i e₁ e′)
+    ≤⟨ ℕₚ.⊔-mono-≤ (substAt-pres-callDepth i e e′) (substAt-pres-callDepth i e₁ e′) ⟩
+  callDepth e′ ⊔ callDepth e ⊔ (callDepth e′ ⊔ callDepth e₁)
+    ≡⟨ ⊔-solve 3 (λ a b c → (a ⊕ b) ⊕ (a ⊕ c) ⊜ a ⊕ (b ⊕ c)) refl (callDepth e′) (callDepth e) (callDepth e₁) ⟩
+  callDepth e′ ⊔ (callDepth e ⊔ callDepth e₁)
+    ∎
+substAt-pres-callDepth i (Code.cast eq e) e′ = substAt-pres-callDepth i e e′
+substAt-pres-callDepth i (Code.- e) e′ = substAt-pres-callDepth i e e′
+substAt-pres-callDepth i (e Code.+ e₁) e′ = begin
+  callDepth (substAt i e e′) ⊔ callDepth (substAt i e₁ e′)
+    ≤⟨ ℕₚ.⊔-mono-≤ (substAt-pres-callDepth i e e′) (substAt-pres-callDepth i e₁ e′) ⟩
+  callDepth e′ ⊔ callDepth e ⊔ (callDepth e′ ⊔ callDepth e₁)
+    ≡⟨ ⊔-solve 3 (λ a b c → (a ⊕ b) ⊕ (a ⊕ c) ⊜ a ⊕ (b ⊕ c)) refl (callDepth e′) (callDepth e) (callDepth e₁) ⟩
+  callDepth e′ ⊔ (callDepth e ⊔ callDepth e₁)
+    ∎
+substAt-pres-callDepth i (e Code.* e₁) e′ = begin
+  callDepth (substAt i e e′) ⊔ callDepth (substAt i e₁ e′)
+    ≤⟨ ℕₚ.⊔-mono-≤ (substAt-pres-callDepth i e e′) (substAt-pres-callDepth i e₁ e′) ⟩
+  callDepth e′ ⊔ callDepth e ⊔ (callDepth e′ ⊔ callDepth e₁)
+    ≡⟨ ⊔-solve 3 (λ a b c → (a ⊕ b) ⊕ (a ⊕ c) ⊜ a ⊕ (b ⊕ c)) refl (callDepth e′) (callDepth e) (callDepth e₁) ⟩
+  callDepth e′ ⊔ (callDepth e ⊔ callDepth e₁)
+    ∎
+substAt-pres-callDepth i (e Code.^ x) e′ = substAt-pres-callDepth i e e′
+substAt-pres-callDepth i (e Code.>> x) e′ = substAt-pres-callDepth i e e′
+substAt-pres-callDepth i (Code.rnd e) e′ = substAt-pres-callDepth i e e′
+substAt-pres-callDepth i (Code.fin x e) e′ = substAt-pres-callDepth i e e′
+substAt-pres-callDepth i (Code.asInt e) e′ = substAt-pres-callDepth i e e′
+substAt-pres-callDepth i Code.nil e′ = ℕₚ.m≤n⊔m (callDepth e′) 0
+substAt-pres-callDepth i (Code.cons e e₁) e′ = begin
+  callDepth (substAt i e e′) ⊔ callDepth (substAt i e₁ e′)
+    ≤⟨ ℕₚ.⊔-mono-≤ (substAt-pres-callDepth i e e′) (substAt-pres-callDepth i e₁ e′) ⟩
+  callDepth e′ ⊔ callDepth e ⊔ (callDepth e′ ⊔ callDepth e₁)
+    ≡⟨ ⊔-solve 3 (λ a b c → (a ⊕ b) ⊕ (a ⊕ c) ⊜ a ⊕ (b ⊕ c)) refl (callDepth e′) (callDepth e) (callDepth e₁) ⟩
+  callDepth e′ ⊔ (callDepth e ⊔ callDepth e₁)
+    ∎
+substAt-pres-callDepth i (Code.head e) e′ = substAt-pres-callDepth i e e′
+substAt-pres-callDepth i (Code.tail e) e′ = substAt-pres-callDepth i e e′
+substAt-pres-callDepth i (Code.call f es) e′ = begin
+  suc (funCallDepth f) ⊔ callDepth′ (substAt′ i es e′)
+    ≤⟨ ℕₚ.⊔-monoʳ-≤ (suc (funCallDepth f)) (helper es) ⟩
+  suc (funCallDepth f) ⊔ (callDepth e′ ⊔ callDepth′ es)
+    ≡⟨ ⊔-solve 3 (λ a b c → b ⊕ (a ⊕ c) ⊜ a ⊕ (b ⊕ c)) refl (callDepth e′) (suc (funCallDepth f)) (callDepth′ es) ⟩
+  callDepth e′ ⊔ (suc (funCallDepth f) ⊔ callDepth′ es)
+    ∎
+  where
+  helper : ∀ {n ts} (es : All _ {n} ts) → callDepth′ (substAt′ i es e′) ℕ.≤ callDepth e′ ⊔ callDepth′ es
+  helper []       = ℕₚ.m≤n⊔m (callDepth e′) 0
+  helper (e ∷ es) = begin
+    callDepth (substAt i e e′) ⊔ callDepth′ (substAt′ i es e′)
+      ≤⟨ ℕₚ.⊔-mono-≤ (substAt-pres-callDepth i e e′) (helper es) ⟩
+    callDepth e′ ⊔ callDepth e ⊔ (callDepth e′ ⊔ callDepth′ es)
+      ≡⟨ ⊔-solve 3 (λ a b c → ((a ⊕ b) ⊕ (a ⊕ c)) ⊜ (a ⊕ (b ⊕ c))) refl (callDepth e′) (callDepth e) (callDepth′ es) ⟩
+    callDepth e′ ⊔ (callDepth e ⊔ callDepth′ es)
+      ∎
+substAt-pres-callDepth i (Code.if e then e₁ else e₂) e′ = begin
+  callDepth (substAt i e e′) ⊔ callDepth (substAt i e₁ e′) ⊔ callDepth (substAt i e₂ e′)
+    ≤⟨ ℕₚ.⊔-mono-≤ (ℕₚ.⊔-mono-≤ (substAt-pres-callDepth i e e′) (substAt-pres-callDepth i e₁ e′)) (substAt-pres-callDepth i e₂ e′) ⟩
+  callDepth e′ ⊔ callDepth e ⊔ (callDepth e′ ⊔ callDepth e₁) ⊔ (callDepth e′ ⊔ callDepth e₂)
+    ≡⟨ ⊔-solve 4 (λ a b c d → ((a ⊕ b) ⊕ (a ⊕ c)) ⊕ (a ⊕ d) ⊜ a ⊕ ((b ⊕ c) ⊕ d)) refl (callDepth e′) (callDepth e) (callDepth e₁) (callDepth e₂) ⟩
+  callDepth e′ ⊔ (callDepth e ⊔ callDepth e₁ ⊔ callDepth e₂)
+    ∎
+
+updateRef-pres-callDepth : ∀ {e : Expression Γ t} ref stateless val (e′ : Expression Γ t′) →
+                           callDepth (updateRef {e = e} ref stateless val e′) ℕ.≤ callDepth e ⊔ callDepth val ⊔ callDepth e′
+updateRef-pres-callDepth (state i) stateless val e′ = contradiction (state i) stateless
+updateRef-pres-callDepth (var i) stateless val e′ = substAt-pres-callDepth i e′ val
+updateRef-pres-callDepth (abort e) stateless val e′ = ℕₚ.m≤n⊔m (callDepth e ⊔ callDepth val) (callDepth e′)
+updateRef-pres-callDepth [ ref ] stateless val e′ = updateRef-pres-callDepth ref (stateless ∘ [_]) (unbox val) e′
+updateRef-pres-callDepth (unbox ref) stateless val e′ = updateRef-pres-callDepth ref (stateless ∘ unbox) [ val ] e′
+updateRef-pres-callDepth (splice {e₁ = e₁} {e₂ = e₂} ref ref₁ e₃) stateless val e′ = begin
+  callDepth outer
+    ≤⟨ updateRef-pres-callDepth ref₁ (stateless ∘ (λ x → spliceʳ _ x e₃)) (head (tail (cut val e₃))) inner ⟩
+  callDepth e₂ ⊔ (callDepth val ⊔ callDepth e₃) ⊔ callDepth inner
+    ≤⟨ ℕₚ.⊔-monoʳ-≤ (callDepth e₂ ⊔ (callDepth val ⊔ callDepth e₃)) (updateRef-pres-callDepth ref (stateless ∘ (λ x → spliceˡ x _ e₃)) (head (cut val e₃)) e′) ⟩
+  callDepth e₂ ⊔ (callDepth val ⊔ callDepth e₃) ⊔ (callDepth e₁ ⊔ (callDepth val ⊔ callDepth e₃) ⊔ callDepth e′)
+    ≡⟨ ⊔-solve 5 (λ a b c d e → ((b ⊕ (d ⊕ c)) ⊕ ((a ⊕ (d ⊕ c)) ⊕ e)) ⊜ ((((a ⊕ b) ⊕ c) ⊕ d) ⊕ e)) refl (callDepth e₁) (callDepth e₂) (callDepth e₃) (callDepth val) (callDepth e′) ⟩
+  callDepth e₁ ⊔ callDepth e₂ ⊔ callDepth e₃ ⊔ callDepth val ⊔ callDepth e′
+    ∎
+  where
+  inner = updateRef ref (stateless ∘ (λ x → spliceˡ x _ e₃)) (head (cut val e₃)) e′
+  outer = updateRef ref₁ (stateless ∘ (λ x → spliceʳ _ x e₃)) (head (tail (cut val e₃))) inner
+updateRef-pres-callDepth (cut {e₁ = e₁} ref e₂) stateless val e′ = begin
+  callDepth (updateRef ref (stateless ∘ (λ x → (cut x e₂))) (splice (head val) (head (tail val)) e₂) e′)
+    ≤⟨ updateRef-pres-callDepth ref (stateless ∘ (λ x → (cut x e₂))) (splice (head val) (head (tail val)) e₂) e′ ⟩
+  callDepth e₁ ⊔ (callDepth val ⊔ callDepth val ⊔ callDepth e₂) ⊔ callDepth e′
+    ≡⟨ ⊔-solve 4 (λ a b c d → (a ⊕ ((c ⊕ c) ⊕ b)) ⊕ d ⊜ ((a ⊕ b) ⊕ c) ⊕ d) refl (callDepth e₁) (callDepth e₂) (callDepth val) (callDepth e′) ⟩
+  callDepth e₁ ⊔ callDepth e₂ ⊔ callDepth val ⊔ callDepth e′
+    ∎
+updateRef-pres-callDepth (cast eq ref) stateless val e′ = updateRef-pres-callDepth ref (stateless ∘ cast eq) (cast (sym eq) val) e′
+updateRef-pres-callDepth nil stateless val e′ = ℕₚ.m≤n⊔m (callDepth val) (callDepth e′)
+updateRef-pres-callDepth (cons {e₁ = e₁} {e₂ = e₂} ref ref₁) stateless val e′ = begin
+  callDepth outer
+    ≤⟨ updateRef-pres-callDepth ref₁ (stateless ∘ consʳ e₁) (tail val) inner ⟩
+  callDepth e₂ ⊔ callDepth val ⊔ callDepth inner
+    ≤⟨ ℕₚ.⊔-monoʳ-≤ (callDepth e₂ ⊔ callDepth val) (updateRef-pres-callDepth ref (stateless ∘ (λ x → consˡ x e₂)) (head val) e′) ⟩
+  callDepth e₂ ⊔ callDepth val ⊔ (callDepth e₁ ⊔ callDepth val ⊔ callDepth e′)
+    ≡⟨ ⊔-solve 4 (λ a b c d → (b ⊕ c) ⊕ ((a ⊕ c) ⊕ d) ⊜ ((a ⊕ b) ⊕ c) ⊕ d) refl (callDepth e₁) (callDepth e₂) (callDepth val) (callDepth e′) ⟩
+  callDepth e₁ ⊔ callDepth e₂ ⊔ callDepth val ⊔ callDepth e′
+    ∎
+  where
+  inner = updateRef ref (stateless ∘ (λ x → consˡ x e₂)) (head val) e′
+  outer = updateRef ref₁ (stateless ∘ consʳ e₁) (tail val) inner
+updateRef-pres-callDepth (head {e = e} ref) stateless val e′ = begin
+  callDepth (updateRef ref (stateless ∘ head) (cons val (tail e)) e′)
+    ≤⟨ updateRef-pres-callDepth ref (stateless ∘ head) (cons val (tail e)) e′ ⟩
+  callDepth e ⊔ (callDepth val ⊔ callDepth e) ⊔ callDepth e′
+    ≡⟨ ⊔-solve 3 (λ a b c → (a ⊕ (b ⊕ a)) ⊕ c ⊜ (a ⊕ b) ⊕ c) refl (callDepth e) (callDepth val) (callDepth e′) ⟩
+  callDepth e ⊔ callDepth val ⊔ callDepth e′
+    ∎
+updateRef-pres-callDepth (tail {e = e} ref) stateless val e′ = begin
+  callDepth (updateRef ref (stateless ∘ tail) (cons (head e) val) e′)
+    ≤⟨ updateRef-pres-callDepth ref (stateless ∘ tail) (cons (head e) val) e′ ⟩
+  callDepth e ⊔ (callDepth e ⊔ callDepth val) ⊔ callDepth e′
+    ≡⟨ ⊔-solve 3 (λ a b c → (a ⊕ (a ⊕ b)) ⊕ c ⊜ (a ⊕ b) ⊕ c) refl (callDepth e) (callDepth val) (callDepth e′) ⟩
+  callDepth e ⊔ callDepth val ⊔ callDepth e′
+    ∎
+
+subst-pres-callDepth : ∀ (e : Expression Γ t) (args : All (Expression Δ) Γ) → callDepth (subst e args) ℕ.≤ callDepth e ⊔ callDepth′ args
+subst-pres-callDepth (lit x) args = ℕ.z≤n
+subst-pres-callDepth (state i) args = ℕ.z≤n
+subst-pres-callDepth (var i) args = helper i args
+  where
+  helper : ∀ i (es : All (Expression Γ) Δ) → callDepth (All.lookup i es) ℕ.≤ callDepth′ es
+  helper 0F (e ∷ es) = ℕₚ.m≤m⊔n (callDepth e) (callDepth′ es)
+  helper (suc i) (e ∷ es) = ℕₚ.m≤n⇒m≤o⊔n (callDepth e) (helper i es)
+subst-pres-callDepth (abort e) args = subst-pres-callDepth e args
+subst-pres-callDepth (e ≟ e₁) args = begin
+  callDepth (subst e args) ⊔ callDepth (subst e₁ args)
+    ≤⟨ ℕₚ.⊔-mono-≤ (subst-pres-callDepth e args) (subst-pres-callDepth e₁ args) ⟩
+  callDepth e ⊔ callDepth′ args ⊔ (callDepth e₁ ⊔ callDepth′ args)
+    ≡⟨ ⊔-solve 3 (λ a b c → (a ⊕ c) ⊕ (b ⊕ c) ⊜ (a ⊕ b) ⊕ c) refl (callDepth e) (callDepth e₁) (callDepth′ args) ⟩
+  callDepth e ⊔ callDepth e₁ ⊔ callDepth′ args
+    ∎
+subst-pres-callDepth (e <? e₁) args = begin
+  callDepth (subst e args) ⊔ callDepth (subst e₁ args)
+    ≤⟨ ℕₚ.⊔-mono-≤ (subst-pres-callDepth e args) (subst-pres-callDepth e₁ args) ⟩
+  callDepth e ⊔ callDepth′ args ⊔ (callDepth e₁ ⊔ callDepth′ args)
+    ≡⟨ ⊔-solve 3 (λ a b c → (a ⊕ c) ⊕ (b ⊕ c) ⊜ (a ⊕ b) ⊕ c) refl (callDepth e) (callDepth e₁) (callDepth′ args) ⟩
+  callDepth e ⊔ callDepth e₁ ⊔ callDepth′ args
+    ∎
+subst-pres-callDepth (inv e) args = subst-pres-callDepth e args
+subst-pres-callDepth (e && e₁) args = begin
+  callDepth (subst e args) ⊔ callDepth (subst e₁ args)
+    ≤⟨ ℕₚ.⊔-mono-≤ (subst-pres-callDepth e args) (subst-pres-callDepth e₁ args) ⟩
+  callDepth e ⊔ callDepth′ args ⊔ (callDepth e₁ ⊔ callDepth′ args)
+    ≡⟨ ⊔-solve 3 (λ a b c → (a ⊕ c) ⊕ (b ⊕ c) ⊜ (a ⊕ b) ⊕ c) refl (callDepth e) (callDepth e₁) (callDepth′ args) ⟩
+  callDepth e ⊔ callDepth e₁ ⊔ callDepth′ args
+    ∎
+subst-pres-callDepth (e || e₁) args = begin
+  callDepth (subst e args) ⊔ callDepth (subst e₁ args)
+    ≤⟨ ℕₚ.⊔-mono-≤ (subst-pres-callDepth e args) (subst-pres-callDepth e₁ args) ⟩
+  callDepth e ⊔ callDepth′ args ⊔ (callDepth e₁ ⊔ callDepth′ args)
+    ≡⟨ ⊔-solve 3 (λ a b c → (a ⊕ c) ⊕ (b ⊕ c) ⊜ (a ⊕ b) ⊕ c) refl (callDepth e) (callDepth e₁) (callDepth′ args) ⟩
+  callDepth e ⊔ callDepth e₁ ⊔ callDepth′ args
+    ∎
+subst-pres-callDepth (not e) args = subst-pres-callDepth e args
+subst-pres-callDepth (e and e₁) args = begin
+  callDepth (subst e args) ⊔ callDepth (subst e₁ args)
+    ≤⟨ ℕₚ.⊔-mono-≤ (subst-pres-callDepth e args) (subst-pres-callDepth e₁ args) ⟩
+  callDepth e ⊔ callDepth′ args ⊔ (callDepth e₁ ⊔ callDepth′ args)
+    ≡⟨ ⊔-solve 3 (λ a b c → (a ⊕ c) ⊕ (b ⊕ c) ⊜ (a ⊕ b) ⊕ c) refl (callDepth e) (callDepth e₁) (callDepth′ args) ⟩
+  callDepth e ⊔ callDepth e₁ ⊔ callDepth′ args
+    ∎
+subst-pres-callDepth (e or e₁) args = begin
+  callDepth (subst e args) ⊔ callDepth (subst e₁ args)
+    ≤⟨ ℕₚ.⊔-mono-≤ (subst-pres-callDepth e args) (subst-pres-callDepth e₁ args) ⟩
+  callDepth e ⊔ callDepth′ args ⊔ (callDepth e₁ ⊔ callDepth′ args)
+    ≡⟨ ⊔-solve 3 (λ a b c → (a ⊕ c) ⊕ (b ⊕ c) ⊜ (a ⊕ b) ⊕ c) refl (callDepth e) (callDepth e₁) (callDepth′ args) ⟩
+  callDepth e ⊔ callDepth e₁ ⊔ callDepth′ args
+    ∎
+subst-pres-callDepth [ e ] args = subst-pres-callDepth e args
+subst-pres-callDepth (unbox e) args = subst-pres-callDepth e args
+subst-pres-callDepth (splice e e₁ e₂) args = begin
+  callDepth (subst e args) ⊔ callDepth (subst e₁ args) ⊔ callDepth (subst e₂ args)
+    ≤⟨ ℕₚ.⊔-mono-≤ (ℕₚ.⊔-mono-≤ (subst-pres-callDepth e args) (subst-pres-callDepth e₁ args)) (subst-pres-callDepth e₂ args) ⟩
+  callDepth e ⊔ callDepth′ args ⊔ (callDepth e₁ ⊔ callDepth′ args) ⊔ (callDepth e₂ ⊔ callDepth′ args)
+    ≡⟨ ⊔-solve 4 (λ a b c d → ((a ⊕ d) ⊕ (b ⊕ d)) ⊕ (c ⊕ d) ⊜ ((a ⊕ b) ⊕ c) ⊕ d) refl (callDepth e) (callDepth e₁) (callDepth e₂) (callDepth′ args) ⟩
+  callDepth e ⊔ callDepth e₁ ⊔ callDepth e₂ ⊔ callDepth′ args
+    ∎
+subst-pres-callDepth (cut e e₁) args = begin
+  callDepth (subst e args) ⊔ callDepth (subst e₁ args)
+    ≤⟨ ℕₚ.⊔-mono-≤ (subst-pres-callDepth e args) (subst-pres-callDepth e₁ args) ⟩
+  callDepth e ⊔ callDepth′ args ⊔ (callDepth e₁ ⊔ callDepth′ args)
+    ≡⟨ ⊔-solve 3 (λ a b c → (a ⊕ c) ⊕ (b ⊕ c) ⊜ (a ⊕ b) ⊕ c) refl (callDepth e) (callDepth e₁) (callDepth′ args) ⟩
+  callDepth e ⊔ callDepth e₁ ⊔ callDepth′ args
+    ∎
+subst-pres-callDepth (cast eq e) args = subst-pres-callDepth e args
+subst-pres-callDepth (- e) args = subst-pres-callDepth e args
+subst-pres-callDepth (e + e₁) args = begin
+  callDepth (subst e args) ⊔ callDepth (subst e₁ args)
+    ≤⟨ ℕₚ.⊔-mono-≤ (subst-pres-callDepth e args) (subst-pres-callDepth e₁ args) ⟩
+  callDepth e ⊔ callDepth′ args ⊔ (callDepth e₁ ⊔ callDepth′ args)
+    ≡⟨ ⊔-solve 3 (λ a b c → (a ⊕ c) ⊕ (b ⊕ c) ⊜ (a ⊕ b) ⊕ c) refl (callDepth e) (callDepth e₁) (callDepth′ args) ⟩
+  callDepth e ⊔ callDepth e₁ ⊔ callDepth′ args
+    ∎
+subst-pres-callDepth (e * e₁) args = begin
+  callDepth (subst e args) ⊔ callDepth (subst e₁ args)
+    ≤⟨ ℕₚ.⊔-mono-≤ (subst-pres-callDepth e args) (subst-pres-callDepth e₁ args) ⟩
+  callDepth e ⊔ callDepth′ args ⊔ (callDepth e₁ ⊔ callDepth′ args)
+    ≡⟨ ⊔-solve 3 (λ a b c → (a ⊕ c) ⊕ (b ⊕ c) ⊜ (a ⊕ b) ⊕ c) refl (callDepth e) (callDepth e₁) (callDepth′ args) ⟩
+  callDepth e ⊔ callDepth e₁ ⊔ callDepth′ args
+    ∎
+subst-pres-callDepth (e ^ x) args = subst-pres-callDepth e args
+subst-pres-callDepth (e >> x) args = subst-pres-callDepth e args
+subst-pres-callDepth (rnd e) args = subst-pres-callDepth e args
+subst-pres-callDepth (fin x e) args = subst-pres-callDepth e args
+subst-pres-callDepth (asInt e) args = subst-pres-callDepth e args
+subst-pres-callDepth nil args = ℕ.z≤n
+subst-pres-callDepth (cons e e₁) args = begin
+  callDepth (subst e args) ⊔ callDepth (subst e₁ args)
+    ≤⟨ ℕₚ.⊔-mono-≤ (subst-pres-callDepth e args) (subst-pres-callDepth e₁ args) ⟩
+  callDepth e ⊔ callDepth′ args ⊔ (callDepth e₁ ⊔ callDepth′ args)
+    ≡⟨ ⊔-solve 3 (λ a b c → (a ⊕ c) ⊕ (b ⊕ c) ⊜ (a ⊕ b) ⊕ c) refl (callDepth e) (callDepth e₁) (callDepth′ args) ⟩
+  callDepth e ⊔ callDepth e₁ ⊔ callDepth′ args
+    ∎
+subst-pres-callDepth (head e) args = subst-pres-callDepth e args
+subst-pres-callDepth (tail e) args = subst-pres-callDepth e args
+subst-pres-callDepth (call f es) args = begin
+  suc (funCallDepth f) ⊔ callDepth′ (subst′ es args)
+    ≤⟨ ℕₚ.⊔-monoʳ-≤ (suc (funCallDepth f)) (helper es args) ⟩
+  suc (funCallDepth f) ⊔ (callDepth′ es ⊔ callDepth′ args)
+    ≡⟨ ⊔-solve 3 (λ a b c → a ⊕ (b ⊕ c) ⊜ (a ⊕ b) ⊕ c) refl (suc (funCallDepth f)) (callDepth′ es) (callDepth′ args) ⟩
+  suc (funCallDepth f) ⊔ callDepth′ es ⊔ callDepth′ args
+    ∎
+  where
+  helper : ∀ {n ts} (es : All (Expression Γ) {n} ts) (args : All (Expression Δ) Γ) → callDepth′ (subst′ es args) ℕ.≤ callDepth′ es ℕ.⊔ callDepth′ args
+  helper []       args = ℕ.z≤n
+  helper (e ∷ es) args = begin
+    callDepth (subst e args) ⊔ callDepth′ (subst′ es args)
+      ≤⟨ ℕₚ.⊔-mono-≤ (subst-pres-callDepth e args) (helper es args) ⟩
+    callDepth e ⊔ callDepth′ args ⊔ (callDepth′ es ⊔ callDepth′ args)
+      ≡⟨ ⊔-solve 3 (λ a b c → (a ⊕ c) ⊕ (b ⊕ c) ⊜ (a ⊕ b) ⊕ c) refl (callDepth e) (callDepth′ es) (callDepth′ args) ⟩
+    callDepth e ⊔ callDepth′ es ⊔ callDepth′ args
+      ∎
+subst-pres-callDepth (if e then e₁ else e₂) args = begin
+  callDepth (subst e args) ⊔ callDepth (subst e₁ args) ⊔ callDepth (subst e₂ args)
+    ≤⟨ ℕₚ.⊔-mono-≤ (ℕₚ.⊔-mono-≤ (subst-pres-callDepth e args) (subst-pres-callDepth e₁ args)) (subst-pres-callDepth e₂ args) ⟩
+  callDepth e ⊔ callDepth′ args ⊔ (callDepth e₁ ⊔ callDepth′ args) ⊔ (callDepth e₂ ⊔ callDepth′ args)
+    ≡⟨ ⊔-solve 4 (λ a b c d → ((a ⊕ d) ⊕ (b ⊕ d)) ⊕ (c ⊕ d) ⊜ ((a ⊕ b) ⊕ c) ⊕ d) refl (callDepth e) (callDepth e₁) (callDepth e₂) (callDepth′ args) ⟩
+  callDepth e ⊔ callDepth e₁ ⊔ callDepth e₂ ⊔ callDepth′ args
+    ∎
+
+wkn-pres-callDepth : ∀ t i (s : Statement Γ) → stmtCallDepth (wknStatementAt t i s) ≡ stmtCallDepth s
+wkn-pres-callDepth t i (s Code.∙ s₁) = cong₂ _⊔_ (wkn-pres-callDepth t i s) (wkn-pres-callDepth t i s₁)
+wkn-pres-callDepth t i Code.skip = refl
+wkn-pres-callDepth t i (ref Code.≔ x) = cong₂ _⊔_ (wknAt-pres-callDepth i ref) (wknAt-pres-callDepth i x)
+wkn-pres-callDepth t i (Code.declare x s) = cong₂ _⊔_ (wknAt-pres-callDepth i x) (wkn-pres-callDepth t (suc i) s)
+wkn-pres-callDepth t i (Code.invoke p es) = cong (procCallDepth p ⊔_) (wknAt′-pres-callDepth i es)
+wkn-pres-callDepth t i (Code.if x then s) = cong₂ _⊔_ (wknAt-pres-callDepth i x) (wkn-pres-callDepth t i s)
+wkn-pres-callDepth t i (Code.if x then s else s₁) = congₙ 3 (λ m n o → m ⊔ n ⊔ o) (wknAt-pres-callDepth i x) (wkn-pres-callDepth t i s) (wkn-pres-callDepth t i s₁)
+wkn-pres-callDepth t i (Code.for m s) = wkn-pres-callDepth t (suc i) s
+
+private
+  index₀ : Statement Γ → ℕ
+  index₀ (s ∙ s₁)                                     = index₀ s ℕ.+ index₀ s₁
+  index₀ skip                                         = 0
+  index₀ (ref ≔ x)                                    = 0
+  index₀ (declare x s)                                = index₀ s
+  index₀ (invoke p es)                                = 0
+  index₀ (if x then s)                                = index₀ s
+  index₀ (if x then s else s₁)                        = suc (index₀ s ℕ.+ index₀ s₁)
+  index₀ (for m s)                                    = index₀ s
+
+  index₁ : Statement Γ → ℕ
+  index₁ (s ∙ s₁)              = suc (index₁ s ℕ.+ index₁ s₁)
+  index₁ skip                  = 0
+  index₁ (ref ≔ x)             = 0
+  index₁ (declare x s)         = index₁ s
+  index₁ (invoke x x₁)         = 0
+  index₁ (if x then s)         = suc (3 ℕ.* index₁ s)
+  index₁ (if x then s else s₁) = suc (3 ℕ.* index₁ s ℕ.+ index₁ s₁)
+  index₁ (for m s)             = suc (index₁ s)
+
+  index₂ : Statement Γ → ℕ
+  index₂ (s ∙ s₁)              = 0
+  index₂ skip                  = 0
+  index₂ (ref ≔ x)             = 0
+  index₂ (declare x s)         = suc (index₂ s)
+  index₂ (invoke _ _)          = 0
+  index₂ (if x then s)         = 2 ℕ.* index₂ s
+  index₂ (if x then s else s₁) = 0
+  index₂ (for m s)             = 0
+
+  wkn-pres-index₀ : ∀ t i s → index₀ (wknStatementAt {Γ = Γ} t i s) ≡ index₀ s
+  wkn-pres-index₀ _ i (s ∙ s₁) = cong₂ ℕ._+_ (wkn-pres-index₀ _ i s) (wkn-pres-index₀ _ i s₁)
+  wkn-pres-index₀ _ i skip = refl
+  wkn-pres-index₀ _ i (ref ≔ x) = refl
+  wkn-pres-index₀ _ i (declare x s) = wkn-pres-index₀ _ (suc i) s
+  wkn-pres-index₀ _ i (invoke x x₁) = refl
+  wkn-pres-index₀ _ i (if x then s) = wkn-pres-index₀ _ i s
+  wkn-pres-index₀ _ i (if x then s else s₁) = cong₂ (λ m n → suc (m ℕ.+ n)) (wkn-pres-index₀ _ i s) (wkn-pres-index₀ _ i s₁)
+  wkn-pres-index₀ _ i (for m s) = wkn-pres-index₀ _ (suc i) s
+
+  wkn-pres-index₁ : ∀ t i s → index₁ (wknStatementAt {Γ = Γ} t i s) ≡ index₁ s
+  wkn-pres-index₁ _ i (s ∙ s₁) = cong₂ (λ m n → suc (m ℕ.+ n)) (wkn-pres-index₁ _ i s) (wkn-pres-index₁ _ i s₁)
+  wkn-pres-index₁ _ i skip = refl
+  wkn-pres-index₁ _ i (ref ≔ x) = refl
+  wkn-pres-index₁ _ i (declare x s) = wkn-pres-index₁ _ (suc i) s
+  wkn-pres-index₁ _ i (invoke x x₁) = refl
+  wkn-pres-index₁ _ i (if x then s) = cong (λ m → suc (3 ℕ.* m)) (wkn-pres-index₁ _ i s)
+  wkn-pres-index₁ _ i (if x then s else s₁) = cong₂ (λ m n → suc (3 ℕ.* m ℕ.+ n)) (wkn-pres-index₁ _ i s) (wkn-pres-index₁ _ i s₁)
+  wkn-pres-index₁ _ i (for m s) = cong suc (wkn-pres-index₁ _ (suc i) s)
+
+  wkn-pres-changes : ∀ t i {s} → ChangesState (wknStatementAt {Γ = Γ} t i s) → ChangesState s
+  wkn-pres-changes t i {_ ∙ _} (s ∙ˡ s₁) = wkn-pres-changes t i s ∙ˡ _
+  wkn-pres-changes t i {_ ∙ _} (s ∙ʳ s₁) = _ ∙ʳ wkn-pres-changes t i s₁
+  wkn-pres-changes t i {_ ≔ _} (_≔_ ref {canAssign} {refsState} e) = _≔_ _ {refsState = fromWitness (wknAt-pres-stateless i (toWitness refsState))} _
+  wkn-pres-changes t i {declare _ _} (declare e s) = declare _ (wkn-pres-changes t (suc i) s)
+  wkn-pres-changes t i {invoke _ _} (invoke p es) = invoke _ _
+  wkn-pres-changes t i {if _ then _} (if e then s) = if _ then wkn-pres-changes t i s
+  wkn-pres-changes t i {if _ then _ else _} (if e then′ s else s₁) = if _ then′ wkn-pres-changes t i s else _
+  wkn-pres-changes t i {if _ then _ else _} (if e then s else′ s₁) = if _ then _ else′ wkn-pres-changes t i s₁
+  wkn-pres-changes t i {for _ _} (for m s) = for m (wkn-pres-changes t (suc i) s)
+
+  RecItem : Set
+  RecItem = ∃ λ n → ∃ (Statement {n})
+
+  inlinePredicate : RecItem → Set
+  inlinePredicate (_ , Γ , s) = ¬ ChangesState s → ∀ {ret} → (e : Expression Γ ret) → ∃ λ (e′ : Expression Γ ret) → callDepth e′ ℕ.≤ stmtCallDepth s ⊔ callDepth e
+
+  inlineRel : RecItem → RecItem → Set
+  inlineRel = Lex.×-Lex _≡_ ℕ._<_ (Lex.×-Lex _≡_ ℕ._<_ ℕ._<_) on < (index₀ ∘ proj₂ ∘ proj₂) , < (index₁ ∘ proj₂ ∘ proj₂) , (index₂ ∘ proj₂ ∘ proj₂) > >
+
+  inlineRelWf : Wf.WellFounded inlineRel
+  inlineRelWf =
+    On.wellFounded
+      < (index₀ ∘ proj₂ ∘ proj₂) , < (index₁ ∘ proj₂ ∘ proj₂) , (index₂ ∘ proj₂ ∘ proj₂) > >
+      (Lex.×-wellFounded ℕᵢ.<-wellFounded (Lex.×-wellFounded ℕᵢ.<-wellFounded ℕᵢ.<-wellFounded))
+
+  s<s∙s₁ : ∀ (s s₁ : Statement Γ) → inlineRel (_ , _ , s) (_ , _ , (s ∙ s₁))
+  s<s∙s₁ s s₁ = case index₀ s₁ return (λ x → index₀ s ℕ.< index₀ s ℕ.+ x ⊎ index₀ s ≡ index₀ s ℕ.+ x × (index₁ s ℕ.< suc (index₁ s ℕ.+ index₁ s₁) ⊎ (index₁ s ≡ suc (index₁ s ℕ.+ index₁ s₁) × index₂ s ℕ.< 0))) of λ
+    { 0       → inj₂ (sym (ℕₚ.+-identityʳ (index₀ s)) , inj₁ (ℕₚ.m≤m+n (suc (index₁ s)) (index₁ s₁)))
+    ; (suc n) → inj₁ (ℕₚ.m<m+n (index₀ s) ℕₚ.0<1+n)
+    }
+
+  s₁<s∙s₁ : ∀ (s s₁ : Statement Γ) → inlineRel (_ , _ , s₁) (_ , _ , (s ∙ s₁))
+  s₁<s∙s₁ s s₁ = case index₀ s return (λ x → index₀ s₁ ℕ.< x ℕ.+ index₀ s₁ ⊎ index₀ s₁ ≡ x ℕ.+ index₀ s₁ × (index₁ s₁ ℕ.< suc (index₁ s ℕ.+ index₁ s₁) ⊎ (index₁ s₁ ≡ suc (index₁ s ℕ.+ index₁ s₁) × index₂ s₁ ℕ.< 0))) of λ
+    { 0       → inj₂ (refl , inj₁ (ℕ.s≤s (ℕₚ.m≤n+m (index₁ s₁) (index₁ s))))
+    ; (suc n) → inj₁ (ℕₚ.m<n+m (index₀ s₁) ℕₚ.0<1+n)
+    }
+
+  s<declare‿s : ∀ (s : Statement _) (e : Expression Γ t) → inlineRel (_ , _ , s) (_ , _ , declare e s)
+  s<declare‿s s _ = inj₂ (refl , inj₂ (refl , ℕₚ.n<1+n (index₂ s)))
+
+  splitIf : ∀ (x : Expression Γ bool) (s s₁ : Statement Γ) → Statement Γ
+  splitIf x s s₁ = declare x (if var 0F then wknStatementAt bool 0F s ∙ if var 0F then wknStatementAt bool 0F s₁)
+
+  splitIf<if‿s∙s₁ : ∀ (x : Expression Γ bool) (s s₁ : Statement Γ) → inlineRel (_ , _ , splitIf x s s₁) (_ , _ , (if x then (s ∙ s₁)))
+  splitIf<if‿s∙s₁ x s s₁ = inj₂ (s≡₀s′ , inj₁ s<₁s′)
+    where
+    open +-*-Solver using (solve; _:*_; _:+_; con; _:=_)
+    s≡₀s′ = cong₂ ℕ._+_ (wkn-pres-index₀ bool 0F s) (wkn-pres-index₀ bool 0F s₁)
+    s<₁s′ = begin-strict
+      suc (suc (3 ℕ.* index₁ (wknStatementAt bool 0F s)) ℕ.+ suc (3 ℕ.* index₁ (wknStatementAt bool 0F s₁)))
+        ≡⟨ cong₂ (λ m n → suc (suc (3 ℕ.* m) ℕ.+ suc (3 ℕ.* n))) (wkn-pres-index₁ bool 0F s) (wkn-pres-index₁ bool 0F s₁) ⟩
+      suc (suc (3 ℕ.* index₁ s) ℕ.+ suc (3 ℕ.* index₁ s₁))
+        <⟨ ℕₚ.m<n+m (suc (suc (3 ℕ.* index₁ s) ℕ.+ suc (3 ℕ.* index₁ s₁))) (ℕₚ.0<1+n {n = 0}) ⟩
+      suc (suc (suc (3 ℕ.* index₁ s) ℕ.+ suc (3 ℕ.* index₁ s₁)))
+        ≡⟨ solve 2 (λ m n → con 2 :+ (con 1 :+ (con 3 :* m) :+ (con 1 :+ (con 3 :* n))) := con 1 :+ (con 3 :* (con 1 :+ m :+ n))) refl (index₁ s) (index₁ s₁) ⟩
+      suc (3 ℕ.* (suc (index₁ s ℕ.+ index₁ s₁)))
+        ∎
+
+  splitIf-stateless : ∀ {x : Expression Γ bool} {s s₁ : Statement Γ} → ¬ ChangesState (if x then (s ∙ s₁)) → ¬ ChangesState (splitIf x s s₁)
+  splitIf-stateless stateless (declare _ ((if _ then s) ∙ˡ _))  = stateless (if _ then (wkn-pres-changes bool 0F s ∙ˡ _))
+  splitIf-stateless stateless (declare _ (_ ∙ʳ (if _ then s₁))) = stateless (if _ then (_ ∙ʳ wkn-pres-changes bool 0F s₁))
+
+  pushRef-stateless : ∀ {e} {ref : Expression Γ t} {canAssign val} → ¬ ChangesState (if e then _≔_ ref {canAssign} val) → ¬ ChangesState (_≔_ ref {canAssign} (if e then val else ref))
+  pushRef-stateless stateless (_≔_ ref {refsState = refsState} _) = stateless (if _ then _≔_ ref {refsState = refsState} _)
+
+  declare∘if<if∘declare : ∀ e (e′ : Expression Γ t) s → inlineRel (_ , _ , declare e′ (if wknAt 0F e then s)) (_ , _ , (if e then declare e′ s))
+  declare∘if<if∘declare e e′ s = inj₂ (refl , inj₂ (refl , (begin-strict
+    suc (2 ℕ.* index₂ s)
+      <⟨ ℕₚ.n<1+n _ ⟩
+    suc (suc (2 ℕ.* index₂ s))
+      ≡⟨ solve 1 (λ m → con 2 :+ con 2 :* m := con 2 :* (con 1 :+ m)) refl (index₂ s) ⟩
+    2 ℕ.* suc (index₂ s)
+      ∎)))
+    where
+    open +-*-Solver using (solve; _:*_; _:+_; con; _:=_)
+
+  declare∘if-stateless : ∀ {e} {e′ : Expression Γ t} {s} → ¬ ChangesState (if e then declare e′ s) → ¬ ChangesState (declare e′ (if wknAt 0F e then s))
+  declare∘if-stateless stateless (declare _ (if _ then s)) = stateless (if _ then (declare _ s))
+
+  if<if∘if : ∀ (e e′ : Expression Γ bool) s → inlineRel (_ , _ , (if e && e′ then s)) (_ , _ , (if e then if e′ then s))
+  if<if∘if e e′ s = inj₂ (refl , inj₁ (begin-strict
+    suc (3 ℕ.* index₁ s)
+      <⟨ ℕₚ.m<n+m (suc (3 ℕ.* index₁ s)) (ℕₚ.0<1+n {n = 2}) ⟩
+    4 ℕ.+ 3 ℕ.* index₁ s
+      ≤⟨ ℕₚ.m≤n+m (4 ℕ.+ 3 ℕ.* index₁ s) (6 ℕ.* index₁ s) ⟩
+    6 ℕ.* index₁ s ℕ.+ (4 ℕ.+ 3 ℕ.* index₁ s)
+      ≡⟨ solve 1 (λ m → con 6 :* m :+ (con 4 :+ con 3 :* m) := con 1 :+ con 3 :* (con 1 :+ con 3 :* m)) refl (index₁ s) ⟩
+    suc (3 ℕ.* suc (3 ℕ.* index₁ s))
+      ∎))
+    where
+    open +-*-Solver using (solve; _:*_; _:+_; con; _:=_)
+
+  if-stateless : ∀ {e e′ : Expression Γ bool} {s} → ¬ ChangesState (if e then if e′ then s) → ¬ ChangesState (if e && e′ then s)
+  if-stateless stateless (if _ then s) = stateless (if _ then if _ then s)
+
+  if∙if : ∀ (e e′ : Expression Γ bool) (s s₁ : Statement Γ) → Statement Γ
+  if∙if e e′ s s₁ =
+    declare e (
+    declare (wknAt 0F e′) (
+      if var 1F && var 0F then wknStatementAt bool 0F (wknStatementAt bool 0F s) ∙
+      if var 1F && inv (var 0F) then wknStatementAt bool 0F (wknStatementAt bool 0F s₁)))
+
+  if∙if<if‿if‿else : ∀ (e e′ : Expression Γ bool) s s₁ → inlineRel (_ , _ , if∙if e e′ s s₁) (_ , _ , (if e then (if e′ then s else s₁)))
+  if∙if<if‿if‿else e e′ s s₁ = inj₁ (begin-strict
+    index₀ (wknStatementAt bool 0F (wknStatementAt bool 0F s)) ℕ.+ index₀ (wknStatementAt bool 0F (wknStatementAt bool 0F s₁))
+      ≡⟨ cong₂ ℕ._+_ (wkn-pres-index₀ bool 0F (wknStatementAt bool 0F s)) (wkn-pres-index₀ bool 0F (wknStatementAt bool 0F s₁)) ⟩
+    index₀ (wknStatementAt bool 0F s) ℕ.+ index₀ (wknStatementAt bool 0F s₁)
+      ≡⟨ cong₂ ℕ._+_ (wkn-pres-index₀ bool 0F s) (wkn-pres-index₀ bool 0F s₁) ⟩
+    index₀ s ℕ.+ index₀ s₁
+      <⟨ ℕₚ.n<1+n (index₀ s ℕ.+ index₀ s₁) ⟩
+    suc (index₀ s ℕ.+ index₀ s₁)
+      ∎)
+
+  if∙if-stateless : ∀ {e e′ : Expression Γ bool} {s s₁} → ¬ ChangesState (if e then (if e′ then s else s₁)) → ¬ ChangesState (if∙if e e′ s s₁)
+  if∙if-stateless stateless (declare _ (declare _ ((if _ then s) ∙ˡ _))) = stateless (if _ then (if _ then′ wkn-pres-changes bool 0F (wkn-pres-changes bool 0F s) else _))
+  if∙if-stateless stateless (declare _ (declare _ (_ ∙ʳ (if _ then s₁)))) = stateless (if _ then (if _ then _ else′ wkn-pres-changes bool 0F (wkn-pres-changes bool 0F s₁)))
+
+  declare-stateless : ∀ {i : Fin m} {s : Statement (fin m ∷ Γ)} → ¬ ChangesState (for m s) → ¬ ChangesState (declare (lit (i ′f)) s)
+  declare-stateless stateless (declare _ s) = stateless (for _ s)
+
+  for‿if : ∀ (e : Expression Γ bool) m (s : Statement (fin m ∷ Γ)) → Statement Γ
+  for‿if e m s = declare e (for m (if var 1F then wknStatementAt bool 1F s))
+
+  for‿if<if‿for : ∀ (e : Expression Γ bool) m s → inlineRel (_ , _ , for‿if e m s) (_ , _ , (if e then for m s))
+  for‿if<if‿for e m s = inj₂ (s≡₀s′ , inj₁ s<₁s′)
+    where
+    open +-*-Solver using (solve; _:*_; _:+_; con; _:=_)
+    s≡₀s′ = wkn-pres-index₀ bool 1F s
+    s<₁s′ = begin-strict
+      suc (suc (3 ℕ.* index₁ (wknStatementAt bool 1F s)))
+        ≡⟨ cong (λ m → suc (suc (3 ℕ.* m))) (wkn-pres-index₁ bool 1F s) ⟩
+      suc (suc (3 ℕ.* index₁ s))
+        <⟨ ℕₚ.m<n+m (suc (suc (3 ℕ.* index₁ s))) (ℕₚ.0<1+n {n = 1}) ⟩
+      4 ℕ.+ 3 ℕ.* index₁ s
+        ≡⟨ solve 1 (λ m → con 4 :+ con 3 :* m := con 1 :+ con 3 :* (con 1 :+ m)) refl (index₁ s) ⟩
+      suc (3 ℕ.* suc (index₁ s))
+        ∎
+
+  for‿if-stateless : ∀ {e : Expression Γ bool} {m s} → ¬ ChangesState (if e then for m s) → ¬ ChangesState (for‿if e m s)
+  for‿if-stateless stateless (declare _ (for _ (if _ then s))) = stateless (if _ then (for _ (wkn-pres-changes bool 1F s)))
+
+  if∙if′ : ∀ (e : Expression Γ bool) (s s₁ : Statement Γ) → Statement Γ
+  if∙if′ e s s₁ = declare e (
+    if var 0F then wknStatementAt bool 0F s ∙
+    if inv (var 0F) then wknStatementAt bool 0F s₁)
+
+  if∙if′<if‿else : ∀ (e : Expression Γ bool) s s₁ → inlineRel (_ , _ , if∙if′ e s s₁) (_ , _ , (if e then s else s₁))
+  if∙if′<if‿else e s s₁ = inj₁ (begin-strict
+    index₀ (wknStatementAt bool 0F s) ℕ.+ index₀ (wknStatementAt bool 0F s₁)
+      ≡⟨ cong₂ ℕ._+_ (wkn-pres-index₀ bool 0F s) (wkn-pres-index₀ bool 0F s₁) ⟩
+    index₀ s ℕ.+ index₀ s₁
+      <⟨ ℕₚ.n<1+n (index₀ s ℕ.+ index₀ s₁) ⟩
+    suc (index₀ s ℕ.+ index₀ s₁)
+      ∎)
+
+  if∙if′-stateless : ∀ {e : Expression Γ bool} {s s₁} → ¬ ChangesState (if e then s else s₁) → ¬ ChangesState (if∙if′ e s s₁)
+  if∙if′-stateless stateless (declare _ ((if _ then s) ∙ˡ _)) = stateless (if _ then′ wkn-pres-changes bool 0F s else _)
+  if∙if′-stateless stateless (declare _ (_ ∙ʳ (if _ then s₁))) = stateless (if _ then _ else′ wkn-pres-changes bool 0F s₁)
+
+  inlineHelper : ∀ n,Γ,s → Wf.WfRec inlineRel inlinePredicate n,Γ,s → inlinePredicate n,Γ,s
+  proj₁ (inlineHelper (_ , _ , (s ∙ s₁)) rec stateless e) =
+    proj₁ (rec
+      (_ , _ , s₁)
+      (s₁<s∙s₁ s s₁)
+      (stateless ∘ (s ∙ʳ_))
+      (proj₁ (rec
+        (_ , _ , s)
+        (s<s∙s₁ s s₁)
+        (stateless ∘ (_∙ˡ s₁))
+        e)))
+  proj₁ (inlineHelper (_ , _ , skip) rec stateless e) = e
+  proj₁ (inlineHelper (_ , _ , (_≔_ ref {canAssign} val)) rec stateless e) =
+    updateRef
+      (toWitness canAssign)
+      (stateless ∘ λ x → _≔_ ref {refsState = fromWitness x} val)
+      val
+      e
+  proj₁ (inlineHelper (_ , _ , declare x s) rec stateless e) =
+    elimAt 0F
+      (proj₁ (rec
+        (_ , _ , s)
+        (s<declare‿s s x)
+        (stateless ∘ declare x)
+        (wknAt 0F e)))
+      x
+  proj₁ (inlineHelper (_ , _ , invoke p es) rec stateless e) = contradiction (invoke p es) stateless
+  proj₁ (inlineHelper (_ , _ , (if x then (s ∙ s₁))) rec stateless e) =
+    proj₁ (rec
+      (_ , _ , splitIf x s s₁)
+      (splitIf<if‿s∙s₁ x s s₁)
+      (splitIf-stateless stateless)
+      e)
+  proj₁ (inlineHelper (_ , _ , (if x then skip)) rec stateless e) = e
+  proj₁ (inlineHelper (_ , _ , (if x then (_≔_ ref {canAssign} val))) rec stateless e) =
+    proj₁ (rec
+      (_ , _ , (_≔_ ref {canAssign} (if x then val else ref)))
+      (inj₂ (refl , inj₁ ℕₚ.0<1+n))
+      (pushRef-stateless stateless)
+      e)
+  proj₁ (inlineHelper (_ , _ , (if x then declare x₁ s)) rec stateless e) =
+    proj₁ (rec
+      (_ , _ , declare x₁ (if wknAt 0F x then s))
+      (declare∘if<if∘declare x x₁ s)
+      (declare∘if-stateless stateless)
+      e)
+  proj₁ (inlineHelper (_ , _ , (if x then invoke p es)) rec stateless e) = contradiction (if x then invoke p es) stateless
+  proj₁ (inlineHelper (_ , _ , (if x then if x₁ then s)) rec stateless e) =
+    proj₁ (rec
+      (_ , _ , (if (x && x₁) then s))
+      (if<if∘if x x₁ s)
+      (if-stateless stateless)
+      e)
+  proj₁ (inlineHelper (_ , _ , (if x then (if x₁ then s else s₁))) rec stateless e) =
+    proj₁ (rec
+      (_ , _ , if∙if x x₁ s s₁)
+      (if∙if<if‿if‿else x x₁ s s₁)
+      (if∙if-stateless stateless)
+      e)
+  proj₁ (inlineHelper (_ , _ , (if x then for m s)) rec stateless e) =
+    proj₁ (rec
+      (_ , _ , for‿if x m s)
+      (for‿if<if‿for x m s)
+      (for‿if-stateless stateless)
+      e)
+  proj₁ (inlineHelper (_ , _ , (if x then s else s₁)) rec stateless e) =
+    proj₁ (rec
+      (_ , _ , if∙if′ x s s₁)
+      (if∙if′<if‿else x s s₁)
+      (if∙if′-stateless stateless)
+      e)
+  proj₁ (inlineHelper (_ , _ , for m s) rec stateless e) =
+    Vec.foldl
+      (λ _ → Expression _ _)
+      (λ e i →
+        proj₁ (rec
+          (_ , _ , declare (lit (i ′f)) s)
+          (inj₂ (refl , inj₁ (ℕₚ.n<1+n (index₁ s))))
+          (declare-stateless stateless)
+          e))
+      e
+      (Vec.allFin _)
+  proj₂ (inlineHelper (_ , _ , (s ∙ s₁)) rec stateless e) = begin
+    callDepth (proj₁ outer)
+      ≤⟨ proj₂ outer ⟩
+    stmtCallDepth s₁ ⊔ callDepth (proj₁ inner)
+      ≤⟨ ℕₚ.⊔-monoʳ-≤ (stmtCallDepth s₁) (proj₂ inner) ⟩
+    stmtCallDepth s₁ ⊔ (stmtCallDepth s ⊔ callDepth e)
+      ≡⟨ ⊔-solve 3 (λ a b c → b ⊕ (a ⊕ c) ⊜ (a ⊕ b) ⊕ c) refl (stmtCallDepth s) (stmtCallDepth s₁) (callDepth e) ⟩
+    stmtCallDepth s ⊔ stmtCallDepth s₁ ⊔ callDepth e
+      ∎
+    where
+    inner = rec (_ , _ , s) (s<s∙s₁ s s₁) (stateless ∘ (_∙ˡ s₁)) e
+    outer = rec (_ , _ , s₁) (s₁<s∙s₁ s s₁) (stateless ∘ (s ∙ʳ_)) (proj₁ inner)
+  -- with rec (_ , _ , s) (s<s∙s₁ s s₁) (stateless ∘ (_∙ˡ s₁)) e
+  -- ... | inner , eq with inner | eq | rec (_ , _ , s₁) (s₁<s∙s₁ s s₁) (stateless ∘ (s ∙ʳ_)) inner
+  -- ... | inner | inj₁ inner≤s | outer , inj₁ outer≤s₁ = inj₁ (ℕₚ.m≤n⇒m≤o⊔n (stmtCallDepth s) outer≤s₁)
+  -- ... | inner | inj₁ inner≤s | outer , inj₂ outer≡inner = inj₁ (begin
+  --   callDepth outer ≡⟨ outer≡inner ⟩
+  --   callDepth inner ≤⟨ ℕₚ.m≤n⇒m≤n⊔o (stmtCallDepth s₁) inner≤s ⟩
+  --   stmtCallDepth s ⊔ stmtCallDepth s₁ ∎)
+  -- ... | inner | inj₂ inner≡e | outer , inj₁ outer≤s₁ = inj₁ (ℕₚ.m≤n⇒m≤o⊔n (stmtCallDepth s) outer≤s₁)
+  -- ... | inner | inj₂ inner≡e | outer , inj₂ outer≡inner = inj₂ (trans outer≡inner inner≡e)
+  proj₂ (inlineHelper (_ , _ , skip) rec stateless e) = ℕₚ.≤-refl
+  proj₂ (inlineHelper (_ , _ , (_≔_ ref {canAssign} x)) rec stateless e) = updateRef-pres-callDepth (toWitness canAssign) (λ x → stateless (_≔_ _ {refsState = fromWitness x} _)) x e
+  proj₂ (inlineHelper (_ , _ , declare x s) rec stateless e) = begin
+    callDepth (elimAt 0F (proj₁ inner) x)
+      ≤⟨ elimAt-pres-callDepth 0F (proj₁ inner) x ⟩
+    callDepth x ⊔ callDepth (proj₁ inner)
+      ≤⟨ ℕₚ.⊔-monoʳ-≤ (callDepth x) (proj₂ inner) ⟩
+    callDepth x ⊔ (stmtCallDepth s ⊔ callDepth (wknAt 0F e))
+      ≡⟨ cong (λ m → callDepth x ⊔ (stmtCallDepth s ⊔ m)) (wknAt-pres-callDepth 0F e) ⟩
+    callDepth x ⊔ (stmtCallDepth s ⊔ callDepth e)
+      ≡⟨ ⊔-solve 3 (λ a b c → a ⊕ (b ⊕ c) ⊜ (a ⊕ b) ⊕ c) refl (callDepth x) (stmtCallDepth s) (callDepth e) ⟩
+    callDepth x ⊔ stmtCallDepth s ⊔ callDepth e
+      ∎
+    where
+    inner = rec (_ , _ , s) (s<declare‿s s x) (λ x → stateless (declare _ x)) (wknAt 0F e)
+  proj₂ (inlineHelper (_ , _ , invoke p es) rec stateless e) = contradiction (invoke p es) stateless
+  proj₂ (inlineHelper (_ , _ , (if x then (s ∙ s₁))) rec stateless e) = begin
+    callDepth (proj₁ inner)
+      ≤⟨ proj₂ inner ⟩
+    callDepth x ⊔ (stmtCallDepth (wknStatementAt bool 0F s) ⊔ stmtCallDepth (wknStatementAt bool 0F s₁)) ⊔ callDepth e
+      ≡⟨ cong₂ (λ m n → callDepth x ⊔ (m ⊔ n) ⊔ callDepth e) (wkn-pres-callDepth bool 0F s) (wkn-pres-callDepth bool 0F s₁) ⟩
+    callDepth x ⊔ (stmtCallDepth s ⊔ stmtCallDepth s₁) ⊔ callDepth e
+      ∎
+    where
+    inner = rec (_ , _ , splitIf x s s₁) (splitIf<if‿s∙s₁ x s s₁) (splitIf-stateless stateless) e
+  proj₂ (inlineHelper (_ , _ , (if x then skip)) rec stateless e) = ℕₚ.m≤n⊔m (callDepth x ⊔ 0) (callDepth e)
+  proj₂ (inlineHelper (_ , _ , (if x then (_≔_ ref {canAssign} val))) rec stateless e) = begin
+    callDepth (proj₁ inner)
+      ≤⟨ proj₂ inner ⟩
+    callDepth ref ⊔ (callDepth x ⊔ callDepth val ⊔ callDepth ref) ⊔ callDepth e
+      ≡⟨ ⊔-solve 4 (λ a b c d → (b ⊕ ((a ⊕ c) ⊕ b)) ⊕ d ⊜ (a ⊕ (b ⊕ c)) ⊕ d) refl (callDepth x) (callDepth ref) (callDepth val) (callDepth e) ⟩
+    callDepth x ⊔ (callDepth ref ⊔ callDepth val) ⊔ callDepth e
+      ∎
+    where
+    inner = rec (_ , _ , (_≔_ ref {canAssign} (if x then val else ref))) (inj₂ (refl , inj₁ ℕₚ.0<1+n)) (pushRef-stateless stateless) e
+  proj₂ (inlineHelper (_ , _ , (if x then declare x₁ s)) rec stateless e) = begin
+    callDepth(proj₁ inner)
+      ≤⟨ proj₂ inner ⟩
+    callDepth x₁ ⊔ (callDepth (wknAt 0F x) ⊔ stmtCallDepth s) ⊔ callDepth e
+      ≡⟨ cong (λ m → callDepth x₁ ⊔ (m ⊔ stmtCallDepth s) ⊔ callDepth e) (wknAt-pres-callDepth 0F x) ⟩
+    callDepth x₁ ⊔ (callDepth x ⊔ stmtCallDepth s) ⊔ callDepth e
+      ≡⟨ ⊔-solve 4 (λ a b c d → (b ⊕ (a ⊕ c)) ⊕ d ⊜ (a ⊕ (b ⊕ c)) ⊕ d) refl (callDepth x) (callDepth x₁) (stmtCallDepth s) (callDepth e) ⟩
+    callDepth x ⊔ (callDepth x₁ ⊔ stmtCallDepth s) ⊔ callDepth e
+      ∎
+    where
+    inner = rec (_ , _ , declare x₁ (if wknAt 0F x then s)) (declare∘if<if∘declare x x₁ s) (declare∘if-stateless stateless) e
+  proj₂ (inlineHelper (_ , _ , (if x then invoke p es)) rec stateless e) = contradiction (if _ then invoke p es) stateless
+  proj₂ (inlineHelper (_ , _ , (if x then (if x₁ then s))) rec stateless e) = begin
+    callDepth (proj₁ inner)
+      ≤⟨ proj₂ inner ⟩
+    callDepth x ⊔ callDepth x₁ ⊔ stmtCallDepth s ⊔ callDepth e
+      ≡⟨ ⊔-solve 4 (λ a b c d → ((a ⊕ b) ⊕ c) ⊕ d ⊜ (a ⊕ (b ⊕ c)) ⊕ d) refl (callDepth x) (callDepth x₁) (stmtCallDepth s) (callDepth e) ⟩
+    callDepth x ⊔ (callDepth x₁ ⊔ stmtCallDepth s) ⊔ callDepth e
+      ∎
+    where
+    inner = rec (_ , _ , (if x && x₁ then s)) (if<if∘if x x₁ s) (if-stateless stateless) e
+  proj₂ (inlineHelper (_ , _ , (if x then (if x₁ then s else s₁))) rec stateless e) = begin
+    callDepth (proj₁ inner)
+      ≤⟨ proj₂ inner ⟩
+    callDepth x ⊔ (callDepth (wknAt 0F x₁) ⊔ (stmtCallDepth (wknStatementAt bool 0F (wknStatementAt bool 0F s)) ⊔ stmtCallDepth (wknStatementAt bool 0F (wknStatementAt bool 0F s₁)))) ⊔ callDepth e
+      ≡⟨ congₙ 3 (λ m n o → callDepth x ⊔ (m ⊔ (n ⊔ o)) ⊔ callDepth e) (wknAt-pres-callDepth 0F x₁) (trans (wkn-pres-callDepth bool 0F (wknStatementAt bool 0F s)) (wkn-pres-callDepth bool 0F s)) (trans (wkn-pres-callDepth bool 0F (wknStatementAt bool 0F s₁)) (wkn-pres-callDepth bool 0F s₁)) ⟩
+    callDepth x ⊔ (callDepth x₁ ⊔ (stmtCallDepth s ⊔ stmtCallDepth s₁)) ⊔ callDepth e
+      ≡⟨ ⊔-solve 5 (λ a b c d e → (a ⊕ (b ⊕ (c ⊕ d))) ⊕ e ⊜ (a ⊕ ((b ⊕ c) ⊕ d)) ⊕ e) refl (callDepth x) (callDepth x₁) (stmtCallDepth s) (stmtCallDepth s₁) (callDepth e) ⟩
+    callDepth x ⊔ (callDepth x₁ ⊔ stmtCallDepth s ⊔ stmtCallDepth s₁) ⊔ callDepth e
+      ∎
+    where
+    inner = rec (_ , _ , if∙if x x₁ s s₁) (if∙if<if‿if‿else x x₁ s s₁) (if∙if-stateless stateless) e
+  proj₂ (inlineHelper (_ , _ , (if x then for m s)) rec stateless e) = begin
+    callDepth (proj₁ inner)
+      ≤⟨ proj₂ inner ⟩
+    callDepth x ⊔ stmtCallDepth (wknStatementAt bool 1F s) ⊔ callDepth e
+      ≡⟨ cong (λ m → callDepth x ⊔ m ⊔ callDepth e) (wkn-pres-callDepth bool 1F s) ⟩
+    callDepth x ⊔ stmtCallDepth s ⊔ callDepth e
+      ∎
+    where
+    inner = rec (_ , _ , for‿if x m s) (for‿if<if‿for x m s) (for‿if-stateless stateless) e
+  proj₂ (inlineHelper (_ , _ , (if x then s else s₁)) rec stateless e) = begin
+    callDepth (proj₁ inner)
+      ≤⟨ proj₂ inner ⟩
+    callDepth x ⊔ (stmtCallDepth (wknStatementAt bool 0F s) ⊔ stmtCallDepth (wknStatementAt bool 0F s₁)) ⊔ callDepth e
+      ≡⟨ cong₂ (λ m n → callDepth x ⊔ (m ⊔ n) ⊔ callDepth e) (wkn-pres-callDepth bool 0F s) (wkn-pres-callDepth bool 0F s₁) ⟩
+    callDepth x ⊔ (stmtCallDepth s ⊔ stmtCallDepth s₁) ⊔ callDepth e
+      ≡⟨ ⊔-solve 4 (λ a b c d → (a ⊕ (b ⊕ c)) ⊕ d ⊜ ((a ⊕ b) ⊕ c) ⊕ d) refl (callDepth x) (stmtCallDepth s) (stmtCallDepth s₁) (callDepth e) ⟩
+    callDepth x ⊔ stmtCallDepth s ⊔ stmtCallDepth s₁ ⊔ callDepth e
+      ∎
+    where
+    inner = rec (_ , _ , if∙if′ x s s₁) (if∙if′<if‿else x s s₁) (if∙if′-stateless stateless) e
+  proj₂ (inlineHelper (n , Γ , for m s) rec stateless {ret} e) = helper
+    (stmtCallDepth s)
+    (λ e i →
+      rec
+      (_ , _ , declare (lit (i ′f)) s)
+      (inj₂ (refl , inj₁ (ℕₚ.n<1+n (index₁ s))))
+      (declare-stateless stateless)
+      e)
+    e
+    (Vec.allFin m)
+    where
+    helper : ∀ {n m} k (f : ∀ {n : ℕ} e (i : Fin m) → ∃ λ e′ → callDepth e′ ℕ.≤ k ⊔ callDepth e) → ∀ e xs → callDepth (Vec.foldl (λ _ → Expression Γ ret) {n} (λ {n} e i → proj₁ (f {n} e i)) e xs) ℕ.≤ k ⊔ callDepth e
+    helper k f e []       = ℕₚ.m≤n⊔m k (callDepth e)
+    helper k f e (x ∷ xs) = begin
+      callDepth (Vec.foldl _ (λ e i → proj₁ (f e i)) (proj₁ (f e x)) xs)
+        ≤⟨ helper k f (proj₁ (f e x)) xs ⟩
+      k ⊔ callDepth (proj₁ (f e x))
+        ≤⟨ ℕₚ.⊔-monoʳ-≤ k (proj₂ (f e x)) ⟩
+      k ⊔ (k ⊔ callDepth e)
+        ≡⟨ ⊔-solve 2 (λ a b → a ⊕ (a ⊕ b) ⊜ a ⊕ b) refl k (callDepth e) ⟩
+      k ⊔ callDepth e
+        ∎
+
+inlineFunction : Function Γ ret → All (Expression Δ) Γ → Expression Δ ret
+inlineFunction (declare e f) args = inlineFunction f (subst e args ∷ args)
+inlineFunction (_∙return_ s {stateless} e) args =
+  subst
+    (proj₁ (Wf.All.wfRec
+      inlineRelWf
+      _
+      inlinePredicate
+      inlineHelper
+      (_ , _ , s)
+      (toWitnessFalse stateless)
+      e))
+    args
+
+inlineFunction-lowers-callDepth : ∀ (f : Function Δ ret) (args : All (Expression Γ) Δ) → callDepth (inlineFunction f args) ℕ.≤ funCallDepth f ⊔ callDepth′ args
+inlineFunction-lowers-callDepth (declare e f) args = begin
+  callDepth (inlineFunction f (subst e args ∷ args))
+    ≤⟨ inlineFunction-lowers-callDepth f (subst e args ∷ args) ⟩
+  funCallDepth f ⊔ (callDepth (subst e args) ⊔ callDepth′ args)
+    ≤⟨ ℕₚ.⊔-monoʳ-≤ (funCallDepth f) (ℕₚ.⊔-monoˡ-≤ (callDepth′ args) (subst-pres-callDepth e args)) ⟩
+  funCallDepth f ⊔ (callDepth e ⊔ callDepth′ args ⊔ callDepth′ args)
+    ≡⟨ ⊔-solve 3 (λ a b c → a ⊕ ((b ⊕ c) ⊕ c) ⊜ (a ⊕ b) ⊕ c) refl (funCallDepth f) (callDepth e) (callDepth′ args) ⟩
+  funCallDepth f ⊔ callDepth e ⊔ callDepth′ args
+    ∎
+inlineFunction-lowers-callDepth (_∙return_ s {stateless} e) args = begin
+  callDepth (subst (proj₁ theCall) args)          ≤⟨ subst-pres-callDepth (proj₁ theCall) args ⟩
+  callDepth (proj₁ theCall) ⊔ callDepth′ args     ≤⟨ ℕₚ.⊔-monoˡ-≤ (callDepth′ args) (proj₂ theCall) ⟩
+  stmtCallDepth s ⊔ callDepth e ⊔ callDepth′ args ∎
+  where
+  theCall = Wf.All.wfRec
+    inlineRelWf
+    _
+    inlinePredicate
+    inlineHelper
+    (_ , _ , s)
+    (toWitnessFalse stateless)
+    e
+
+elimFunctions : Expression Γ t → ∃ λ (e : Expression Γ t) → callDepth e ≡ 0
+elimFunctions {Γ = Γ} = Wf.All.wfRec relWf _ pred helper ∘ (_ ,_)
+  where
+  index  : Expression Γ t → ℕ
+  index′ : All (Expression Γ) Δ → ℕ
+
+  index (Code.lit x) = 0
+  index (Code.state i) = 0
+  index (Code.var i) = 0
+  index (Code.abort e) = suc (index e)
+  index (e Code.≟ e₁) = 1 ℕ.+ index e ℕ.+ index e₁
+  index (e Code.<? e₁) = 1 ℕ.+ index e ℕ.+ index e₁
+  index (Code.inv e) = suc (index e)
+  index (e Code.&& e₁) = 1 ℕ.+ index e ℕ.+ index e₁
+  index (e Code.|| e₁) = 1 ℕ.+ index e ℕ.+ index e₁
+  index (Code.not e) = suc (index e)
+  index (e Code.and e₁) = 1 ℕ.+ index e ℕ.+ index e₁
+  index (e Code.or e₁) = 1 ℕ.+ index e ℕ.+ index e₁
+  index Code.[ e ] = suc (index e)
+  index (Code.unbox e) = suc (index e)
+  index (Code.splice e e₁ e₂) = 1 ℕ.+ index e ℕ.+ index e₁ ℕ.+ index e₂
+  index (Code.cut e e₁) = 1 ℕ.+ index e ℕ.+ index e₁
+  index (Code.cast eq e) = suc (index e)
+  index (Code.- e) = suc (index e)
+  index (e Code.+ e₁) = 1 ℕ.+ index e ℕ.+ index e₁
+  index (e Code.* e₁) = 1 ℕ.+ index e ℕ.+ index e₁
+  index (e Code.^ x) = suc (index e)
+  index (e Code.>> x) = suc (index e)
+  index (Code.rnd e) = suc (index e)
+  index (Code.fin x e) = suc (index e)
+  index (Code.asInt e) = suc (index e)
+  index Code.nil = 0
+  index (Code.cons e e₁) = 1 ℕ.+ index e ℕ.+ index e₁
+  index (Code.head e) = suc (index e)
+  index (Code.tail e) = suc (index e)
+  index (Code.call f es) = index′ es
+  index (Code.if e then e₁ else e₂) = 1 ℕ.+ index e ℕ.+ index e₁ ℕ.+ index e₂
+
+  index′ []       = 1
+  index′ (e ∷ es) = index e ℕ.+ index′ es
+
+  pred : ∃ (Expression Γ) → Set
+  pred (t , e) = ∃ λ (e : Expression Γ t) → callDepth e ≡ 0
+
+  pred′ : All (Expression Γ) Δ → Set
+  pred′ {Δ = Δ} _ = ∃ λ (es : All (Expression Γ) Δ) → callDepth′ es ≡ 0
+
+  rel = Lex.×-Lex _≡_ ℕ._<_ ℕ._<_ on < callDepth ∘ proj₂ , index ∘ proj₂ >
+
+  data _<′₁_ : ∃ (Expression Γ) → All (Expression Γ) Δ → Set where
+    inj₁ : {e : Expression Γ t} {es : All (Expression Γ) Δ} → callDepth e ℕ.< callDepth′ es → (t , e) <′₁ es
+    inj₂ : {e : Expression Γ t} {es : All (Expression Γ) Δ} → callDepth e ≡ callDepth′ es → index e ℕ.< index′ es → (t , e) <′₁ es
+
+  data _<′₂_ : ∀ {n ts} → All (Expression Γ) {n} ts → All (Expression Γ) Δ → Set where
+    inj₁ : ∀ {n ts} {es′ : All (Expression Γ) {n} ts} {es : All (Expression Γ) Δ} → callDepth′ es′ ℕ.< callDepth′ es → es′ <′₂ es
+    inj₂ : ∀ {n ts} {es′ : All (Expression Γ) {n} ts} {es : All (Expression Γ) Δ} → callDepth′ es′ ≡ callDepth′ es → index′ es′ ℕ.≤ index′ es → es′ <′₂ es
+
+  <′₁-<′₂-trans : ∀ {n ts} {e : Expression Γ t} {es : All (Expression Γ) Δ} {es′ : All (Expression Γ) {n} ts} →
+                  (t , e) <′₁ es → es <′₂ es′ → (t , e) <′₁ es′
+  <′₁-<′₂-trans (inj₁ <₁) (inj₁ <₂) = inj₁ (ℕₚ.<-trans <₁ <₂)
+  <′₁-<′₂-trans (inj₁ <₁) (inj₂ ≡₂ _) = inj₁ (ℕₚ.<-transˡ <₁ (ℕₚ.≤-reflexive ≡₂))
+  <′₁-<′₂-trans (inj₂ ≡₁ _) (inj₁ <₂) = inj₁ (ℕₚ.<-transʳ (ℕₚ.≤-reflexive ≡₁) <₂)
+  <′₁-<′₂-trans (inj₂ ≡₁ <₁) (inj₂ ≡₂ ≤₂) = inj₂ (trans ≡₁ ≡₂) (ℕₚ.<-transˡ <₁ ≤₂)
+
+  <′₂-trans : ∀ {m n ts ts′} {es : All (Expression Γ) Δ} {es′ : All (Expression Γ) {n} ts} {es′′ : All (Expression Γ) {m} ts′} →
+              es <′₂ es′ → es′ <′₂ es′′ → es <′₂ es′′
+  <′₂-trans (inj₁ <₁) (inj₁ <₂) = inj₁ (ℕₚ.<-trans <₁ <₂)
+  <′₂-trans (inj₁ <₁) (inj₂ ≡₂ _) = inj₁ (ℕₚ.<-transˡ <₁ (ℕₚ.≤-reflexive ≡₂))
+  <′₂-trans (inj₂ ≡₁ _) (inj₁ <₂) = inj₁ (ℕₚ.<-transʳ (ℕₚ.≤-reflexive ≡₁) <₂)
+  <′₂-trans (inj₂ ≡₁ ≤₁) (inj₂ ≡₂ ≤₂) = inj₂ (trans ≡₁ ≡₂) (ℕₚ.≤-trans ≤₁ ≤₂)
+
+  index′>0 : ∀ (es : All (Expression Γ) Δ) → index′ es ℕ.> 0
+  index′>0 []       = ℕₚ.≤-refl
+  index′>0 (e ∷ es) = ℕₚ.<-transˡ (index′>0 es) (ℕₚ.m≤n+m (index′ es) (index e))
+
+  e<′₁es⇒e<f[es] : ∀ {e : Expression Γ t} {es : All (Expression Γ) Δ} → (t , e) <′₁ es → ∀ f → rel (t , e) (t′ , call f es)
+  e<′₁es⇒e<f[es] {e = e} {es} (inj₁ <) f = inj₁ (ℕₚ.<-transˡ < (ℕₚ.m≤n⊔m (suc (funCallDepth f)) (callDepth′ es)))
+  e<′₁es⇒e<f[es] {e = e} {es} (inj₂ ≡ <) f with callDepth′ es | funCallDepth f | ℕ.compare (callDepth′ es) (suc (funCallDepth f))
+  ... | _ | _ | ℕ.less m k = inj₁ (begin
+    suc (callDepth e) ≡⟨ cong suc ≡ ⟩
+    suc m             ≤⟨ ℕₚ.m≤m+n (suc m) k ⟩
+    suc m ℕ.+ k       ≤⟨ ℕₚ.m≤m⊔n (suc m ℕ.+ k) m ⟩
+    suc m ℕ.+ k ⊔ m   ∎)
+  ... | _ | _ | ℕ.equal m = inj₂ (trans ≡ (sym (ℕₚ.⊔-idem m)) , <)
+  ... | _ | _ | ℕ.greater n k = inj₂ ((begin-equality
+    callDepth e       ≡⟨  ≡ ⟩
+    suc n ℕ.+ k       ≡˘⟨ ℕₚ.m≤n⇒m⊔n≡n (ℕₚ.≤-trans (ℕₚ.n≤1+n n) (ℕₚ.m≤m+n (suc n) k)) ⟩
+    n ⊔ (suc n ℕ.+ k) ∎) , <)
+
+  e<ᵢe∷es : ∀ (e : Expression Γ t) (es : All (Expression Γ) Δ) → index e ℕ.< index′ (e ∷ es)
+  e<ᵢe∷es e es = ℕₚ.m<m+n (index e) (index′>0 es)
+
+  e<′₁e∷es : ∀ e (es : All (Expression Γ) Δ) → (t , e) <′₁ (e ∷ es)
+  e<′₁e∷es e es with callDepth e in eq₁ | callDepth′ es in eq₂ | ℕ.compare (callDepth e) (callDepth′ es)
+  ... | _ | _ | ℕ.less m k = inj₁
+    (begin
+      suc (callDepth e)           ≡⟨  cong suc eq₁ ⟩
+      suc m                       ≤⟨  ℕₚ.m≤m+n (suc m) k ⟩
+      suc m ℕ.+ k                 ≤⟨  ℕₚ.m≤n⊔m m (suc m ℕ.+ k) ⟩
+      m ⊔ (suc m ℕ.+ k)           ≡˘⟨ cong₂ _⊔_ eq₁ eq₂ ⟩
+      callDepth e ⊔ callDepth′ es ∎)
+  ... | _ | _ | ℕ.equal m = inj₂
+    (begin-equality
+      callDepth e                 ≡⟨  eq₁ ⟩
+      m                           ≡˘⟨ ℕₚ.⊔-idem m ⟩
+      m ⊔ m                       ≡˘⟨ cong₂ _⊔_ eq₁ eq₂ ⟩
+      callDepth e ⊔ callDepth′ es ∎)
+    (e<ᵢe∷es e es)
+  ... | _ | _ | ℕ.greater n k = inj₂
+    (sym (ℕₚ.m≥n⇒m⊔n≡m (begin
+      callDepth′ es ≡⟨  eq₂ ⟩
+      n             ≤⟨  ℕₚ.n≤1+n n ⟩
+      suc n         ≤⟨  ℕₚ.m≤m+n (suc n) k ⟩
+      suc n ℕ.+ k   ≡˘⟨ eq₁ ⟩
+      callDepth e   ∎)))
+    (e<ᵢe∷es e es)
+
+  es<′₂e∷es : ∀ (e : Expression Γ t) (es : All (Expression Γ) Δ) → es <′₂ (e ∷ es)
+  es<′₂e∷es e es with callDepth e in eq₁ | callDepth′ es in eq₂ | ℕ.compare (callDepth e) (callDepth′ es)
+  ... | _ | _ | ℕ.less m k = inj₂
+    (sym (ℕₚ.m≤n⇒m⊔n≡n (begin
+      callDepth e   ≡⟨  eq₁ ⟩
+      m             ≤⟨  ℕₚ.n≤1+n m ⟩
+      suc m         ≤⟨  ℕₚ.m≤m+n (suc m) k ⟩
+      suc m ℕ.+ k   ≡˘⟨ eq₂ ⟩
+      callDepth′ es ∎)))
+    (ℕₚ.m≤n+m (index′ es) (index e))
+  ... | _ | _ | ℕ.equal m = inj₂
+    (begin-equality
+      callDepth′ es               ≡⟨  eq₂ ⟩
+      m                           ≡˘⟨ ℕₚ.⊔-idem m ⟩
+      m ⊔ m                       ≡˘⟨ cong₂ _⊔_ eq₁ eq₂ ⟩
+      callDepth e ⊔ callDepth′ es ∎)
+    (ℕₚ.m≤n+m (index′ es) (index e))
+  ... | _ | _ | ℕ.greater n k = inj₁
+    (begin
+      suc (callDepth′ es)         ≡⟨ cong suc eq₂ ⟩
+      suc n                       ≤⟨ ℕₚ.m≤m+n (suc n) k ⟩
+      suc n ℕ.+ k                 ≤⟨ ℕₚ.m≤m⊔n (suc n ℕ.+ k) n ⟩
+      suc n ℕ.+ k ⊔ n             ≡˘⟨ cong₂ _⊔_ eq₁ eq₂ ⟩
+      callDepth e ⊔ callDepth′ es ∎)
+
+  relWf = On.wellFounded < callDepth ∘ proj₂ , index ∘ proj₂ > (Lex.×-wellFounded ℕᵢ.<-wellFounded ℕᵢ.<-wellFounded)
+
+  wf′₁ : ∀ f (es : All (Expression Γ) Δ) → Wf.WfRec rel pred (t , call f es) →
+         ∀ t,e → t,e <′₁ es → pred t,e
+  wf′₁ f _ rec (_ , e) r = rec (_ , e) (e<′₁es⇒e<f[es] r f)
+
+  wf′₂ : ∀ f (es : All (Expression Γ) Δ) → Wf.WfRec rel pred (t , call f es) →
+         ∀ {n ts} (es′ : All (Expression Γ) {n} ts) → es′ <′₂ es → pred′ es′
+  wf′₂ _ _ rec []       r = [] , refl
+  wf′₂ f es rec (e ∷ es′) r = proj₁ rec₁ ∷ proj₁ rec₂ , cong₂ _⊔_ (proj₂ rec₁) (proj₂ rec₂)
+    where
+    rec₁ = wf′₁ f es rec (_ , e) (<′₁-<′₂-trans (e<′₁e∷es e es′) r)
+    rec₂ = wf′₂ f es rec es′ (<′₂-trans (es<′₂e∷es e es′) r)
+
+  rec₁ : ∀ (f : Expression Γ t → Expression Γ t′) → (∀ {e} → index (f e) ≡ suc (index e)) → (∀ {e} → callDepth (f e) ≡ callDepth e) → ∀ e → Wf.WfRec rel pred (t′ , f e) → pred (t′ , f e)
+  rec₁ f index-step depth-eq e acc = f (proj₁ inner) , trans depth-eq (proj₂ inner)
+    where inner = acc (_ , e) (inj₂ (sym depth-eq , ℕₚ.≤-reflexive (sym index-step)))
+
+  rec₂ : ∀ {t′′} (f : Expression Γ t → Expression Γ t′ → Expression Γ t′′) → (∀ {e e₁} → index (f e e₁) ≡ suc (index e ℕ.+ index e₁)) → (∀ {e e₁} → callDepth (f e e₁) ≡ callDepth e ⊔ callDepth e₁) → ∀ e e₁ → Wf.WfRec rel pred (t′′ , f e e₁) → pred (t′′ , f e e₁)
+  rec₂ f index-step depth-eq e e₁ acc = f (proj₁ inner) (proj₁ inner₁) , trans depth-eq (cong₂ _⊔_ (proj₂ inner) (proj₂ inner₁))
+    where
+    helper : ∀ a b c d e f → a ≡ b ⊔ c → d ≡ suc (e ℕ.+ f) → (b ℕ.< a ⊎ b ≡ a × e ℕ.< d)
+    helper a b c d e f eq₁ eq₂ with ℕ.compare b a
+    ... | ℕ.less .b k = inj₁ (ℕₚ.m≤m+n (suc b) k)
+    ... | ℕ.equal .a = inj₂ (refl , ℕₚ.m+n≤o⇒m≤o (suc e) (ℕₚ.≤-reflexive (sym eq₂)))
+    ... | ℕ.greater .a k = contradiction (ℕₚ.≤-reflexive (sym eq₁)) (ℕₚ.<⇒≱ (begin-strict
+      a               <⟨ ℕₚ.n<1+n a ⟩
+      suc a           ≤⟨ ℕₚ.m≤m+n (suc a) k ⟩
+      suc a ℕ.+ k     ≤⟨ ℕₚ.m≤m⊔n (suc a ℕ.+ k) c ⟩
+      suc a ℕ.+ k ⊔ c ∎))
+
+    helper₁ : ∀ a b c d e f → a ≡ b ⊔ c → d ≡ suc (e ℕ.+ f) → (c ℕ.< a ⊎ c ≡ a × f ℕ.< d)
+    helper₁ a b c d e f eq₁ eq₂ = helper a c b d f e (trans eq₁ (ℕₚ.⊔-comm b c)) (trans eq₂ (cong suc (ℕₚ.+-comm e f)))
+
+    inner = acc (_ , e) (helper (callDepth (f e e₁)) (callDepth e) (callDepth e₁) (index (f e e₁)) (index e) (index e₁) depth-eq index-step)
+    inner₁ = acc (_ , e₁) (helper₁ (callDepth (f e e₁)) (callDepth e) (callDepth e₁) (index (f e e₁)) (index e) (index e₁) depth-eq index-step)
+
+  rec₃ : ∀ {t′′ t′′′} (f : Expression Γ t → Expression Γ t′ → Expression Γ t′′ → Expression Γ t′′′) → (∀ {e e₁ e₂} → index (f e e₁ e₂) ≡ suc (index e ℕ.+ index e₁ ℕ.+ index e₂)) → (∀ {e e₁ e₂} → callDepth (f e e₁ e₂) ≡ callDepth e ⊔ callDepth e₁ ⊔ callDepth e₂) → ∀ e e₁ e₂ → Wf.WfRec rel pred (t′′′ , f e e₁ e₂) → pred (t′′′ , f e e₁ e₂)
+  rec₃ f index-step depth-eq e e₁ e₂ acc = f (proj₁ inner) (proj₁ inner₁) (proj₁ inner₂) , trans depth-eq (congₙ 3 (λ a b c → a ⊔ b ⊔ c) (proj₂ inner) (proj₂ inner₁) (proj₂ inner₂))
+    where
+    helper : ∀ {a b c d e f g h} → a ≡ b ⊔ c ⊔ d → e ≡ suc (f ℕ.+ g ℕ.+ h) → b ℕ.< a ⊎ b ≡ a × f ℕ.< e
+    helper {a} {b} {c} {d} {e} {f} {g} {h} eq₁ eq₂ with ℕ.compare a b
+    ... | ℕ.less .a k = contradiction (ℕₚ.≤-reflexive (sym eq₁)) (ℕₚ.<⇒≱ (begin-strict
+      a                   <⟨ ℕₚ.n<1+n a ⟩
+      suc a               ≤⟨ ℕₚ.m≤m+n (suc a) k ⟩
+      suc a ℕ.+ k         ≤⟨ ℕₚ.m≤m⊔n (suc a ℕ.+ k) c ⟩
+      suc a ℕ.+ k ⊔ c     ≤⟨ ℕₚ.m≤m⊔n (suc a ℕ.+ k ⊔ c) d ⟩
+      suc a ℕ.+ k ⊔ c ⊔ d ∎))
+    ... | ℕ.equal .a = inj₂ (refl , (begin
+      suc f             ≤⟨  ℕₚ.m≤m+n (suc f) g ⟩
+      suc f ℕ.+ g       ≤⟨  ℕₚ.m≤m+n (suc f ℕ.+ g) h ⟩
+      suc f ℕ.+ g ℕ.+ h ≡˘⟨ eq₂ ⟩
+      e                 ∎))
+    ... | ℕ.greater .b k = inj₁ (ℕₚ.m≤m+n (suc b) k)
+
+    helper₁ : ∀ {a} b {c} d {e} f {g} h → a ≡ b ⊔ c ⊔ d → e ≡ suc (f ℕ.+ g ℕ.+ h) → c ℕ.< a ⊎ c ≡ a × g ℕ.< e
+    helper₁ {a} b {c} d {e} f {g} h eq₁ eq₂ =
+      helper
+        (trans eq₁ (cong (_⊔ d) (ℕₚ.⊔-comm b c)))
+        (trans eq₂ (cong (ℕ._+ h) (cong suc (ℕₚ.+-comm f g))))
+
+    helper₂ : ∀ {a} b c {d e} f g {h} → a ≡ b ⊔ c ⊔ d → e ≡ suc (f ℕ.+ g ℕ.+ h) → d ℕ.< a ⊎ d ≡ a × h ℕ.< e
+    helper₂ {a} b c {d} {e} f g {h} eq₁ eq₂ =
+      helper
+        (trans eq₁ (trans (ℕₚ.⊔-comm (b ⊔ c) d) (sym (ℕₚ.⊔-assoc d b c))))
+        (trans eq₂ (cong suc (trans (ℕₚ.+-comm (f ℕ.+ g) h) (sym (ℕₚ.+-assoc h f g)))))
+
+    inner = acc (_ , e) (helper depth-eq index-step)
+    inner₁ = acc (_ , e₁) (helper₁ (callDepth e) (callDepth e₂) (index e) (index e₂) depth-eq index-step)
+    inner₂ = acc (_ , e₂) (helper₂ (callDepth e) (callDepth e₁) (index e) (index e₁) depth-eq index-step)
+
+  helper : ∀ t,e → Wf.WfRec rel pred t,e → pred t,e
+  helper′ : ∀ (es : All (Expression Γ) Δ) → (∀ (t,e : ∃ (Expression Γ)) → t,e <′₁ es → pred t,e) → (∀ {n ts} (es′ : All (Expression Γ) {n} ts) → es′ <′₂ es  → pred′ es′) → pred′ es
+
+  helper (_ , Code.lit x) acc = lit x , refl
+  helper (_ , Code.state i) acc = state i , refl
+  helper (_ , Code.var i) acc = var i , refl
+  helper (_ , Code.abort e) acc = rec₁ abort refl refl e acc
+  helper (_ , _≟_ {hasEquality = hasEq} e e₁) acc = rec₂ (_≟_ {hasEquality = hasEq}) refl refl e e₁ acc
+  helper (_ , _<?_ {isNumeric = isNum} e e₁) acc = rec₂ (_<?_ {isNumeric = isNum}) refl refl e e₁ acc
+  helper (_ , Code.inv e) acc = rec₁ inv refl refl e acc
+  helper (_ , e Code.&& e₁) acc = rec₂ _&&_ refl refl e e₁ acc
+  helper (_ , e Code.|| e₁) acc = rec₂ _||_ refl refl e e₁ acc
+  helper (_ , Code.not e) acc = rec₁ not refl refl e acc
+  helper (_ , e Code.and e₁) acc = rec₂ _and_ refl refl e e₁ acc
+  helper (_ , e Code.or e₁) acc = rec₂ _or_ refl refl e e₁ acc
+  helper (_ , Code.[ e ]) acc = rec₁ [_] refl refl e acc
+  helper (_ , Code.unbox e) acc = rec₁ unbox refl refl e acc
+  helper (_ , Code.splice e e₁ e₂) acc = rec₃ splice refl refl e e₁ e₂ acc
+  helper (_ , Code.cut e e₁) acc = rec₂ cut refl refl e e₁ acc
+  helper (_ , Code.cast eq e) acc = rec₁ (cast eq) refl refl e acc
+  helper (_ , -_ {isNumeric = isNum} e) acc = rec₁ (-_ {isNumeric = isNum}) refl refl e acc
+  helper (_ , e Code.+ e₁) acc = rec₂ _+_ refl refl e e₁ acc
+  helper (_ , e Code.* e₁) acc = rec₂ _*_ refl refl e e₁ acc
+  helper (_ , _^_ {isNumeric = isNum} e x) acc = rec₁ (λ e → _^_ {isNumeric = isNum} e x) refl refl e acc
+  helper (_ , e Code.>> x) acc = rec₁ (_>> x) refl refl e acc
+  helper (_ , Code.rnd e) acc = rec₁ rnd refl refl e acc
+  helper (_ , Code.fin x e) acc = rec₁ (fin x) refl refl e acc
+  helper (_ , Code.asInt e) acc = rec₁ asInt refl refl e acc
+  helper (_ , Code.nil) acc = nil , refl
+  helper (_ , Code.cons e e₁) acc = rec₂ cons refl refl e e₁ acc
+  helper (_ , Code.head e) acc = rec₁ head refl refl e acc
+  helper (_ , Code.tail e) acc = rec₁ tail refl refl e acc
+  helper (_ , Code.call f es) acc =
+    acc
+      (_ , inlineFunction f (proj₁ inner))
+      (inj₁ (begin-strict
+        callDepth (inlineFunction f (proj₁ inner)) ≤⟨ inlineFunction-lowers-callDepth f (proj₁ inner) ⟩
+        funCallDepth f ⊔ callDepth′ (proj₁ inner)  ≡⟨ cong (funCallDepth f ⊔_) (proj₂ inner) ⟩
+        funCallDepth f ⊔ 0                         ≡⟨ ℕₚ.⊔-identityʳ (funCallDepth f) ⟩
+        funCallDepth f                             <⟨ ℕₚ.n<1+n (funCallDepth f) ⟩
+        suc (funCallDepth f)                       ≤⟨ ℕₚ.m≤m⊔n (suc (funCallDepth f)) (callDepth′ es) ⟩
+        suc (funCallDepth f) ⊔ callDepth′ es       ∎))
+    where inner = helper′ es (wf′₁ f es acc) (wf′₂ f es acc)
+  helper (_ , (Code.if e then e₁ else e₂)) acc = rec₃ if_then_else_ refl refl e e₁ e₂ acc
+
+  proj₁ (helper′ [] acc acc′) = []
+  proj₁ (helper′ (e ∷ es) acc acc′) = proj₁ (acc (_ , e) (e<′₁e∷es e es)) ∷ proj₁ (acc′ es (es<′₂e∷es e es))
+  proj₂ (helper′ [] acc acc′) = refl
+  proj₂ (helper′ (e ∷ es) acc acc′) = cong₂ _⊔_ (proj₂ (acc (_ , e) (e<′₁e∷es e es))) (proj₂ (acc′ es (es<′₂e∷es e es)))
diff --git a/src/Helium/Data/Pseudocode/Properties.agda b/src/Helium/Data/Pseudocode/Properties.agda
new file mode 100644
index 0000000..d73b4dd
--- /dev/null
+++ b/src/Helium/Data/Pseudocode/Properties.agda
@@ -0,0 +1,109 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Basic properties of the pseudocode data types
+------------------------------------------------------------------------
+
+{-# OPTIONS --without-K --safe #-}
+
+module Helium.Data.Pseudocode.Properties where
+
+import Data.Nat as ℕ
+open import Data.Product using (_,_; uncurry)
+open import Data.Vec using ([]; _∷_)
+open import Function using (_∋_)
+open import Helium.Data.Pseudocode.Core
+import Relation.Binary.Consequences as Consequences
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; cong₂)
+open import Relation.Nullary using (Dec; yes; no)
+open import Relation.Nullary.Decidable.Core using (map′)
+open import Relation.Nullary.Product using (_×-dec_)
+
+infixl 4 _≟ᵗ_ _≟ˢ_
+
+_≟ᵗ_ : ∀ (t t′ : Type) → Dec (t ≡ t′)
+bool ≟ᵗ bool = yes refl
+bool ≟ᵗ int = no (λ ())
+bool ≟ᵗ fin n = no (λ ())
+bool ≟ᵗ real = no (λ ())
+bool ≟ᵗ bit = no (λ ())
+bool ≟ᵗ bits n = no (λ ())
+bool ≟ᵗ tuple n x = no (λ ())
+bool ≟ᵗ array t′ n = no (λ ())
+int ≟ᵗ bool = no (λ ())
+int ≟ᵗ int = yes refl
+int ≟ᵗ fin n = no (λ ())
+int ≟ᵗ real = no (λ ())
+int ≟ᵗ bit = no (λ ())
+int ≟ᵗ bits n = no (λ ())
+int ≟ᵗ tuple n x = no (λ ())
+int ≟ᵗ array t′ n = no (λ ())
+fin n ≟ᵗ bool = no (λ ())
+fin n ≟ᵗ int = no (λ ())
+fin m ≟ᵗ fin n = map′ (cong fin) (λ { refl → refl }) (m ℕ.≟ n)
+fin n ≟ᵗ real = no (λ ())
+fin n ≟ᵗ bit = no (λ ())
+fin n ≟ᵗ bits n₁ = no (λ ())
+fin n ≟ᵗ tuple n₁ x = no (λ ())
+fin n ≟ᵗ array t′ n₁ = no (λ ())
+real ≟ᵗ bool = no (λ ())
+real ≟ᵗ int = no (λ ())
+real ≟ᵗ fin n = no (λ ())
+real ≟ᵗ real = yes refl
+real ≟ᵗ bit = no (λ ())
+real ≟ᵗ bits n = no (λ ())
+real ≟ᵗ tuple n x = no (λ ())
+real ≟ᵗ array t′ n = no (λ ())
+bit ≟ᵗ bool = no (λ ())
+bit ≟ᵗ int = no (λ ())
+bit ≟ᵗ fin n = no (λ ())
+bit ≟ᵗ real = no (λ ())
+bit ≟ᵗ bit = yes refl
+bit ≟ᵗ bits n = no (λ ())
+bit ≟ᵗ tuple n x = no (λ ())
+bit ≟ᵗ array t n = no (λ ())
+bits n ≟ᵗ bool = no (λ ())
+bits n ≟ᵗ int = no (λ ())
+bits n ≟ᵗ fin n₁ = no (λ ())
+bits n ≟ᵗ real = no (λ ())
+bits m ≟ᵗ bit = no (λ ())
+bits m ≟ᵗ bits n = map′ (cong bits) (λ { refl → refl }) (m ℕ.≟ n)
+bits n ≟ᵗ tuple n₁ x = no (λ ())
+bits n ≟ᵗ array t′ n₁ = no (λ ())
+tuple n x ≟ᵗ bool = no (λ ())
+tuple n x ≟ᵗ int = no (λ ())
+tuple n x ≟ᵗ fin n₁ = no (λ ())
+tuple n x ≟ᵗ real = no (λ ())
+tuple n x ≟ᵗ bit = no (λ ())
+tuple n x ≟ᵗ bits n₁ = no (λ ())
+tuple _ [] ≟ᵗ tuple _ [] = yes refl
+tuple _ [] ≟ᵗ tuple _ (y ∷ ys) = no (λ ())
+tuple _ (x ∷ xs) ≟ᵗ tuple _ [] = no (λ ())
+tuple _ (x ∷ xs) ≟ᵗ tuple _ (y ∷ ys) = map′ (λ { (refl , refl) → refl }) (λ { refl → refl , refl }) (x ≟ᵗ y ×-dec tuple _ xs ≟ᵗ tuple _ ys)
+tuple n x ≟ᵗ array t′ n₁ = no (λ ())
+array t n ≟ᵗ bool = no (λ ())
+array t n ≟ᵗ int = no (λ ())
+array t n ≟ᵗ fin n₁ = no (λ ())
+array t n ≟ᵗ real = no (λ ())
+array t n ≟ᵗ bit = no (λ ())
+array t n ≟ᵗ bits n₁ = no (λ ())
+array t n ≟ᵗ tuple n₁ x = no (λ ())
+array t m ≟ᵗ array t′ n = map′ (uncurry (cong₂ array)) (λ { refl → refl , refl }) (t ≟ᵗ t′ ×-dec m ℕ.≟ n)
+
+_≟ˢ_ : ∀ (t t′ : Sliced) → Dec (t ≡ t′)
+bits ≟ˢ bits = yes refl
+bits ≟ˢ array x = no (λ ())
+array x ≟ˢ bits = no (λ ())
+array x ≟ˢ array y = map′ (cong array) (λ { refl → refl }) (x ≟ᵗ y)
+
+bits-injective : ∀ {m n} → (Type ∋ bits m) ≡ bits n → m ≡ n
+bits-injective refl = refl
+
+array-injective₁ : ∀ {t t′ m n} → (Type ∋ array t m) ≡ array t′ n → t ≡ t′
+array-injective₁ refl = refl
+
+array-injective₂ : ∀ {t t′ m n} → (Type ∋ array t m) ≡ array t′ n → m ≡ n
+array-injective₂ refl = refl
+
+typeEqRecomp : ∀ {t t′} → .(eq : t ≡ t′) → t ≡ t′
+typeEqRecomp = Consequences.dec⇒recomputable _≟ᵗ_
diff --git a/src/Helium/Semantics/Axiomatic/Assertion.agda b/src/Helium/Semantics/Axiomatic/Assertion.agda
new file mode 100644
index 0000000..8192e5f
--- /dev/null
+++ b/src/Helium/Semantics/Axiomatic/Assertion.agda
@@ -0,0 +1,173 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Definition of assertions used in correctness triples
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --without-K #-}
+
+open import Helium.Data.Pseudocode.Types using (RawPseudocode)
+
+module Helium.Semantics.Axiomatic.Assertion
+  {b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃}
+  (rawPseudocode : RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃)
+  where
+
+open RawPseudocode rawPseudocode
+
+open import Data.Bool as Bool using (Bool)
+open import Data.Empty.Polymorphic using (⊥)
+open import Data.Fin as Fin using (suc)
+open import Data.Fin.Patterns
+open import Data.Nat using (ℕ; suc)
+import Data.Nat.Properties as ℕₚ
+open import Data.Product using (∃; _×_; _,_; proj₁; proj₂)
+open import Data.Sum using (_⊎_)
+open import Data.Unit.Polymorphic using (⊤)
+open import Data.Vec as Vec using (Vec; []; _∷_; _++_)
+open import Data.Vec.Relation.Unary.All as All using (All; []; _∷_)
+open import Function using (_$_)
+open import Helium.Data.Pseudocode.Core
+open import Helium.Semantics.Axiomatic.Core rawPseudocode
+open import Helium.Semantics.Axiomatic.Term rawPseudocode as Term using (Term)
+open import Level using (_⊔_; Lift; lift; lower) renaming (suc to ℓsuc)
+
+private
+  variable
+    t t′     : Type
+    m n o    : ℕ
+    Γ Δ Σ ts : Vec Type m
+
+open Term.Term
+
+data Assertion (Σ : Vec Type o) (Γ : Vec Type n) (Δ : Vec Type m) : Set (ℓsuc (b₁ ⊔ i₁ ⊔ r₁))
+
+data Assertion Σ Γ Δ where
+  all    : Assertion Σ Γ (t ∷ Δ) → Assertion Σ Γ Δ
+  some   : Assertion Σ Γ (t ∷ Δ) → Assertion Σ Γ Δ
+  pred   : Term Σ Γ Δ bool → Assertion Σ Γ Δ
+  comb   : ∀ {n} → (Vec (Set (b₁ ⊔ i₁ ⊔ r₁)) n → Set (b₁ ⊔ i₁ ⊔ r₁)) → Vec (Assertion Σ Γ Δ) n → Assertion Σ Γ Δ
+
+substVars : Assertion Σ Γ Δ → All (Term Σ ts Δ) Γ → Assertion Σ ts Δ
+substVars (all P)     ts = all (substVars P (Term.wknMeta′ ts))
+substVars (some P)    ts = some (substVars P (Term.wknMeta′ ts))
+substVars (pred p)    ts = pred (Term.substVars p ts)
+substVars (comb f Ps) ts = comb f (helper Ps ts)
+  where
+  helper : ∀ {n m ts} → Vec (Assertion Σ _ Δ) n → All (Term {n = m} Σ ts Δ) Γ → Vec (Assertion Σ ts Δ) n
+  helper []       ts = []
+  helper (P ∷ Ps) ts = substVars P ts ∷ helper Ps ts
+
+elimVar : Assertion Σ (t ∷ Γ) Δ → Term Σ Γ Δ t → Assertion Σ Γ Δ
+elimVar (all P)          t = all (elimVar P (Term.wknMeta t))
+elimVar (some P)         t = some (elimVar P (Term.wknMeta t))
+elimVar (pred p)         t = pred (Term.elimVar p t)
+elimVar (comb f Ps)      t = comb f (helper Ps t)
+  where
+  helper : ∀ {n} → Vec (Assertion Σ (_ ∷ Γ) Δ) n → Term Σ Γ Δ _ → Vec (Assertion Σ Γ Δ) n
+  helper []       t = []
+  helper (P ∷ Ps) t = elimVar P t ∷ helper Ps t
+
+wknVar : Assertion Σ Γ Δ → Assertion Σ (t ∷ Γ) Δ
+wknVar (all P)          = all (wknVar P)
+wknVar (some P)         = some (wknVar P)
+wknVar (pred p)         = pred (Term.wknVar p)
+wknVar (comb f Ps)      = comb f (helper Ps)
+  where
+  helper : ∀ {n} → Vec (Assertion Σ Γ Δ) n → Vec (Assertion Σ (_ ∷ Γ) Δ) n
+  helper []       = []
+  helper (P ∷ Ps) = wknVar P ∷ helper Ps
+
+wknVars : (ts : Vec Type n) → Assertion Σ Γ Δ → Assertion Σ (ts ++ Γ) Δ
+wknVars τs (all P)          = all (wknVars τs P)
+wknVars τs (some P)         = some (wknVars τs P)
+wknVars τs (pred p)         = pred (Term.wknVars τs p)
+wknVars τs (comb f Ps)      = comb f (helper Ps)
+  where
+  helper : ∀ {n} → Vec (Assertion Σ Γ Δ) n → Vec (Assertion Σ (τs ++ Γ) Δ) n
+  helper []       = []
+  helper (P ∷ Ps) = wknVars τs P ∷ helper Ps
+
+addVars : Assertion Σ [] Δ → Assertion Σ Γ Δ
+addVars (all P)          = all (addVars P)
+addVars (some P)         = some (addVars P)
+addVars (pred p)         = pred (Term.addVars p)
+addVars (comb f Ps)      = comb f (helper Ps)
+  where
+  helper : ∀ {n} → Vec (Assertion Σ [] Δ) n → Vec (Assertion Σ Γ Δ) n
+  helper []       = []
+  helper (P ∷ Ps) = addVars P ∷ helper Ps
+
+wknMetaAt : ∀ i → Assertion Σ Γ Δ → Assertion Σ Γ (Vec.insert Δ i t)
+wknMetaAt i (all P)          = all (wknMetaAt (suc i) P)
+wknMetaAt i (some P)         = some (wknMetaAt (suc i) P)
+wknMetaAt i (pred p)         = pred (Term.wknMetaAt i p)
+wknMetaAt i (comb f Ps)      = comb f (helper i Ps)
+  where
+  helper : ∀ {n} i → Vec (Assertion Σ Γ Δ) n → Vec (Assertion Σ Γ (Vec.insert Δ i _)) n
+  helper i []       = []
+  helper i (P ∷ Ps) = wknMetaAt i P ∷ helper i Ps
+
+-- NOTE: better to induct on P instead of ts?
+wknMetas : (ts : Vec Type n) → Assertion Σ Γ Δ → Assertion Σ Γ (ts ++ Δ)
+wknMetas []       P = P
+wknMetas (_ ∷ ts) P = wknMetaAt 0F (wknMetas ts P)
+
+module _ (2≉0 : Term.2≉0) where
+  -- NOTE: better to induct on e here than in Term?
+  subst : Assertion Σ Γ Δ → {e : Code.Expression Σ Γ t} → Code.CanAssign Σ e → Term Σ Γ Δ t → Assertion Σ Γ Δ
+  subst (all P)          e t = all (subst P e (Term.wknMeta t))
+  subst (some P)         e t = some (subst P e (Term.wknMeta t))
+  subst (pred p)         e t = pred (Term.subst 2≉0 p e t)
+  subst (comb f Ps)      e t = comb f (helper Ps e t)
+    where
+    helper : ∀ {t n} → Vec (Assertion Σ Γ Δ) n → {e : Code.Expression Σ Γ t} → Code.CanAssign Σ e → Term Σ Γ Δ t → Vec (Assertion Σ Γ Δ) n
+    helper []       e t = []
+    helper (P ∷ Ps) e t = subst P e t ∷ helper Ps e t
+
+module Construct where
+  infixl 6 _∧_
+  infixl 5 _∨_
+
+  true : Assertion Σ Γ Δ
+  true = comb (λ _ → ⊤) []
+
+  false : Assertion Σ Γ Δ
+  false = comb (λ _ → ⊥) []
+
+  _∧_ : Assertion Σ Γ Δ → Assertion Σ Γ Δ → Assertion Σ Γ Δ
+  P ∧ Q = comb (λ { (P ∷ Q ∷ []) → P × Q }) (P ∷ Q ∷ [])
+
+  _∨_ : Assertion Σ Γ Δ → Assertion Σ Γ Δ → Assertion Σ Γ Δ
+  P ∨ Q = comb (λ { (P ∷ Q ∷ []) → P ⊎ Q }) (P ∷ Q ∷ [])
+
+  equal : Term Σ Γ Δ t → Term Σ Γ Δ t → Assertion Σ Γ Δ
+  equal {t = bool} x y = pred Term.[ bool ][ x ≟ y ]
+  equal {t = int} x y = pred Term.[ int ][ x ≟ y ]
+  equal {t = fin n} x y = pred Term.[ fin ][ x ≟ y ]
+  equal {t = real} x y = pred Term.[ real ][ x ≟ y ]
+  equal {t = bit} x y = pred Term.[ bit ][ x ≟ y ]
+  equal {t = bits n} x y = pred Term.[ bits ][ x ≟ y ]
+  equal {t = tuple _ []} x y = true
+  equal {t = tuple _ (t ∷ ts)} x y = equal {t = t} (Term.func₁ proj₁ x) (Term.func₁ proj₁ y) ∧ equal (Term.func₁ proj₂ x) (Term.func₁ proj₂ y)
+  equal {t = array t 0} x y = true
+  equal {t = array t (suc n)} x y = all (equal {t = t} (index x) (index y))
+    where
+    index = λ v → Term.unbox (array t) $
+                  Term.func₁ proj₁ $
+                  Term.cut (array t)
+                    (Term.cast (array t) (ℕₚ.+-comm 1 n) (Term.wknMeta v))
+                    (meta 0F)
+
+open Construct public
+
+⟦_⟧ : Assertion Σ Γ Δ → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ Δ ⟧ₜ′ → Set (b₁ ⊔ i₁ ⊔ r₁)
+⟦_⟧′ : Vec (Assertion Σ Γ Δ) n → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ Δ ⟧ₜ′ → Vec (Set (b₁ ⊔ i₁ ⊔ r₁)) n
+
+⟦ all P ⟧ σ γ δ = ∀ x → ⟦ P ⟧ σ γ (x , δ)
+⟦ some P ⟧ σ γ δ = ∃ λ x → ⟦ P ⟧ σ γ (x , δ)
+⟦ pred p ⟧ σ γ δ = Lift (b₁ ⊔ i₁ ⊔ r₁) (Bool.T (lower (Term.⟦ p ⟧ σ γ δ)))
+⟦ comb f Ps ⟧ σ γ δ = f (⟦ Ps ⟧′ σ γ δ)
+
+⟦ [] ⟧′     σ γ δ = []
+⟦ P ∷ Ps ⟧′ σ γ δ = ⟦ P ⟧ σ γ δ ∷ ⟦ Ps ⟧′ σ γ δ
diff --git a/src/Helium/Semantics/Axiomatic/Core.agda b/src/Helium/Semantics/Axiomatic/Core.agda
new file mode 100644
index 0000000..3b7e8db
--- /dev/null
+++ b/src/Helium/Semantics/Axiomatic/Core.agda
@@ -0,0 +1,85 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Base definitions for the axiomatic semantics
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --without-K #-}
+
+open import Helium.Data.Pseudocode.Types using (RawPseudocode)
+
+module Helium.Semantics.Axiomatic.Core
+  {b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃}
+  (rawPseudocode : RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃)
+  where
+
+private
+  open module C = RawPseudocode rawPseudocode
+
+open import Data.Bool as Bool using (Bool)
+open import Data.Fin as Fin using (Fin; zero; suc)
+open import Data.Fin.Patterns
+open import Data.Nat as ℕ using (ℕ; suc)
+import Data.Nat.Induction as Natᵢ
+import Data.Nat.Properties as ℕₚ
+open import Data.Product as × using (_×_; _,_; uncurry)
+open import Data.Sum using (_⊎_)
+open import Data.Unit using (⊤)
+open import Data.Vec as Vec using (Vec; []; _∷_; _++_; lookup)
+open import Data.Vec.Relation.Unary.All as All using (All; []; _∷_)
+open import Function using (_on_)
+open import Helium.Data.Pseudocode.Core
+open import Helium.Data.Pseudocode.Properties
+import Induction.WellFounded as Wf
+open import Level using (_⊔_; Lift; lift)
+import Relation.Binary.Construct.On as On
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; cong₂)
+open import Relation.Nullary using (Dec; does; yes; no)
+open import Relation.Nullary.Decidable.Core using (True; toWitness; map′)
+open import Relation.Nullary.Product using (_×-dec_)
+open import Relation.Unary using (_⊆_)
+
+private
+  variable
+    t t′     : Type
+    m n      : ℕ
+    Γ Δ Σ ts : Vec Type m
+
+⟦_⟧ₜ  : Type → Set (b₁ ⊔ i₁ ⊔ r₁)
+⟦_⟧ₜ′ : Vec Type n → Set (b₁ ⊔ i₁ ⊔ r₁)
+
+⟦ bool ⟧ₜ       = Lift (b₁ ⊔ i₁ ⊔ r₁) Bool
+⟦ int ⟧ₜ        = Lift (b₁ ⊔ r₁) ℤ
+⟦ fin n ⟧ₜ      = Lift (b₁ ⊔ i₁ ⊔ r₁) (Fin n)
+⟦ real ⟧ₜ       = Lift (b₁ ⊔ i₁) ℝ
+⟦ bit ⟧ₜ        = Lift (i₁ ⊔ r₁) Bit
+⟦ bits n ⟧ₜ     = Vec ⟦ bit ⟧ₜ n
+⟦ tuple n ts ⟧ₜ = ⟦ ts ⟧ₜ′ 
+⟦ array t n ⟧ₜ  = Vec ⟦ t ⟧ₜ n
+
+⟦ [] ⟧ₜ′     = Lift (b₁ ⊔ i₁ ⊔ r₁) ⊤
+⟦ t ∷ ts ⟧ₜ′ = ⟦ t ⟧ₜ × ⟦ ts ⟧ₜ′
+
+fetch : ∀ i → ⟦ Γ ⟧ₜ′ → ⟦ lookup Γ i ⟧ₜ
+fetch {Γ = _ ∷ _} 0F      (x , _)  = x
+fetch {Γ = _ ∷ _} (suc i) (_ , xs) = fetch i xs
+
+Transform : Vec Type m → Type → Set (b₁ ⊔ i₁ ⊔ r₁)
+Transform ts t = ⟦ ts ⟧ₜ′ → ⟦ t ⟧ₜ
+
+Predicate : Vec Type m → Set (b₁ ⊔ i₁ ⊔ r₁)
+Predicate ts =  ⟦ ts ⟧ₜ′ → Bool
+
+--   data HoareTriple {n Γ m Δ} : Assertion Σ {n} Γ {m} Δ → Statement Γ → Assertion Σ Γ Δ → Set (b₁ ⊔ i₁ ⊔ r₁) where
+--     _∙_ : ∀ {P Q R s₁ s₂} → HoareTriple P s₁ Q → HoareTriple Q s₂ R → HoareTriple P (s₁ ∙ s₂) R
+--     skip : ∀ {P} → HoareTriple P skip P
+
+--     assign : ∀ {P t ref canAssign e} → HoareTriple (asrtSubst P (toWitness canAssign) (ℰ e)) (_≔_ {t = t} ref {canAssign} e) P
+--     declare : ∀ {t P Q e s} → HoareTriple (P ∧ equal (var 0F) (termWknVar (ℰ e))) s (asrtWknVar Q) → HoareTriple (asrtElimVar P (ℰ e)) (declare {t = t} e s) Q
+--     invoke : ∀ {m ts P Q s e} → HoareTriple (assignMetas Δ ts (All.tabulate var) (asrtAddVars P)) s (asrtAddVars Q) → HoareTriple (assignMetas Δ ts (All.tabulate (λ i → ℰ (All.lookup i e))) (asrtAddVars P)) (invoke {m = m} {ts} (s ∙end) e) (asrtAddVars Q)
+--     if : ∀ {P Q e s₁ s₂} → HoareTriple (P ∧ equal (ℰ e) (𝒦 (Bool.true ′b))) s₁ Q → HoareTriple (P ∧ equal (ℰ e) (𝒦 (Bool.false ′b))) s₂ Q → HoareTriple P (if e then s₁ else s₂) Q
+--     for : ∀ {m} {I : Assertion Σ Γ (fin (suc m) ∷ Δ)} {s} → HoareTriple (some (asrtWknVar (asrtWknMetaAt 1F I) ∧ equal (meta 1F) (var 0F) ∧ equal (meta 0F) (func (λ { _ (lift x ∷ []) → lift (Fin.inject₁ x) }) (meta 1F ∷ [])))) s (some (asrtWknVar (asrtWknMetaAt 1F I) ∧ equal (meta 0F) (func (λ { _ (lift x ∷ []) → lift (Fin.suc x) }) (meta 1F ∷ [])))) → HoareTriple (some (I ∧ equal (meta 0F) (func (λ _ _ → lift 0F) []))) (for m s) (some (I ∧ equal (meta 0F) (func (λ _ _ → lift (Fin.fromℕ m)) [])))
+
+--     consequence : ∀ {P₁ P₂ Q₁ Q₂ s} → ⟦ P₁ ⟧ₐ ⊆ ⟦ P₂ ⟧ₐ → HoareTriple P₂ s Q₂ → ⟦ Q₂ ⟧ₐ ⊆ ⟦ Q₁ ⟧ₐ → HoareTriple P₁ s Q₁
+--     some : ∀ {t P Q s} → HoareTriple P s Q → HoareTriple (some {t = t} P) s (some Q)
+--     frame : ∀ {P Q R s} → HoareTriple P s Q → HoareTriple (P * R) s (Q * R)
diff --git a/src/Helium/Semantics/Axiomatic/Term.agda b/src/Helium/Semantics/Axiomatic/Term.agda
new file mode 100644
index 0000000..2719455
--- /dev/null
+++ b/src/Helium/Semantics/Axiomatic/Term.agda
@@ -0,0 +1,385 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Definition of terms for use in assertions
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --without-K #-}
+
+open import Helium.Data.Pseudocode.Types using (RawPseudocode)
+
+module Helium.Semantics.Axiomatic.Term
+  {b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃}
+  (rawPseudocode : RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃)
+  where
+
+open RawPseudocode rawPseudocode
+
+import Data.Bool as Bool
+open import Data.Fin as Fin using (Fin; suc)
+import Data.Fin.Properties as Finₚ
+open import Data.Fin.Patterns
+open import Data.Nat as ℕ using (ℕ; suc)
+import Data.Nat.Properties as ℕₚ
+open import Data.Product using (∃; _×_; _,_; proj₁; proj₂; uncurry; dmap)
+open import Data.Vec as Vec using (Vec; []; _∷_; _++_; lookup)
+import Data.Vec.Functional as VecF
+import Data.Vec.Properties as Vecₚ
+open import Data.Vec.Relation.Unary.All as All using (All; []; _∷_)
+open import Function using (_∘_; _∘₂_; id; flip)
+open import Helium.Data.Pseudocode.Core
+import Helium.Data.Pseudocode.Manipulate as M
+open import Helium.Semantics.Axiomatic.Core rawPseudocode
+open import Level using (_⊔_; lift; lower)
+open import Relation.Binary.PropositionalEquality hiding ([_]) renaming (subst to ≡-subst)
+open import Relation.Nullary using (does; yes; no; ¬_)
+open import Relation.Nullary.Decidable.Core using (True; toWitness)
+open import Relation.Nullary.Negation using (contradiction)
+
+private
+  variable
+    t t′ t₁ t₂ : Type
+    m n o      : ℕ
+    Γ Δ Σ ts   : Vec Type m
+
+data Term (Σ : Vec Type o) (Γ : Vec Type n) (Δ : Vec Type m) : Type → Set (b₁ ⊔ i₁ ⊔ r₁) where
+  state : ∀ i → Term Σ Γ Δ (lookup Σ i)
+  var   : ∀ i → Term Σ Γ Δ (lookup Γ i)
+  meta  : ∀ i → Term Σ Γ Δ (lookup Δ i)
+  func  : Transform ts t → All (Term Σ Γ Δ) ts → Term Σ Γ Δ t
+
+castType : Term Σ Γ Δ t → t ≡ t′ → Term Σ Γ Δ t′
+castType (state i)   refl = state i
+castType (var i)     refl = var i
+castType (meta i)    refl = meta i
+castType (func f ts) eq   = func (≡-subst (Transform _) eq f) ts
+
+substState : Term Σ Γ Δ t → ∀ i → Term Σ Γ Δ (lookup Σ i) → Term Σ Γ Δ t
+substState (state i) j t′ with i Fin.≟ j
+... | yes refl = t′
+... | no _     = state i
+substState (var i) j t′ = var i
+substState (meta i) j t′ = meta i
+substState (func f ts) j t′ = func f (helper ts j t′)
+  where
+  helper : ∀ {n ts} → All (Term Σ Γ Δ) {n} ts → ∀ i → Term Σ Γ Δ (lookup Σ i) → All (Term Σ Γ Δ) ts
+  helper []       i t′ = []
+  helper (t ∷ ts) i t′ = substState t i t′ ∷ helper ts i t′
+
+substVar : Term Σ Γ Δ t → ∀ i → Term Σ Γ Δ (lookup Γ i) → Term Σ Γ Δ t
+substVar (state i) j t′ = state i
+substVar (var i) j t′ with i Fin.≟ j
+... | yes refl = t′
+... | no _     = var i
+substVar (meta i) j t′ = meta i
+substVar (func f ts) j t′ = func f (helper ts j t′)
+  where
+  helper : ∀ {n ts} → All (Term Σ Γ Δ) {n} ts → ∀ i → Term Σ Γ Δ (lookup Γ i) → All (Term Σ Γ Δ) ts
+  helper []       i t′ = []
+  helper (t ∷ ts) i t′ = substVar t i t′ ∷ helper ts i t′
+
+substVars : Term Σ Γ Δ t → All (Term Σ ts Δ) Γ → Term Σ ts Δ t
+substVars (state i)    ts = state i
+substVars (var i)      ts = All.lookup i ts
+substVars (meta i)     ts = meta i
+substVars (func f ts′) ts = func f (helper ts′ ts)
+  where
+  helper : ∀ {ts ts′} → All (Term Σ Γ Δ) {n} ts → All (Term {n = m} Σ ts′ Δ) Γ → All (Term Σ ts′ Δ) ts
+  helper []        ts = []
+  helper (t ∷ ts′) ts = substVars t ts ∷ helper ts′ ts
+
+elimVar : Term Σ (t′ ∷ Γ) Δ t → Term Σ Γ Δ t′ → Term Σ Γ Δ t
+elimVar (state i)     t′ = state i
+elimVar (var 0F)      t′ = t′
+elimVar (var (suc i)) t′ = var i
+elimVar (meta i)      t′ = meta i
+elimVar (func f ts)   t′ = func f (helper ts t′)
+  where
+  helper : ∀ {n ts} → All (Term Σ (_ ∷ Γ) Δ) {n} ts → Term Σ Γ Δ _ → All (Term Σ Γ Δ) ts
+  helper []       t′ = []
+  helper (t ∷ ts) t′ = elimVar t t′ ∷ helper ts t′
+
+wknVar : Term Σ Γ Δ t → Term Σ (t′ ∷ Γ) Δ t
+wknVar (state i)   = state i
+wknVar (var i)     = var (suc i)
+wknVar (meta i)    = meta i
+wknVar (func f ts) = func f (helper ts)
+  where
+  helper : ∀ {n ts} → All (Term Σ Γ Δ) {n} ts → All (Term Σ (_ ∷ Γ) Δ) ts
+  helper []       = []
+  helper (t ∷ ts) = wknVar t ∷ helper ts
+
+wknVars : (ts : Vec Type n) → Term Σ Γ Δ t → Term Σ (ts ++ Γ) Δ t
+wknVars τs (state i)   = state i
+wknVars τs (var i)     = castType (var (Fin.raise (Vec.length τs) i)) (Vecₚ.lookup-++ʳ τs _ i)
+wknVars τs (meta i)    = meta i
+wknVars τs (func f ts) = func f (helper ts)
+  where
+  helper : ∀ {n ts} → All (Term Σ Γ Δ) {n} ts → All (Term Σ (τs ++ Γ) Δ) ts
+  helper []       = []
+  helper (t ∷ ts) = wknVars τs t ∷ helper ts
+
+addVars : Term Σ [] Δ t → Term Σ Γ Δ t
+addVars (state i)   = state i
+addVars (meta i)    = meta i
+addVars (func f ts) = func f (helper ts)
+  where
+  helper : ∀ {n ts} → All (Term Σ [] Δ) {n} ts → All (Term Σ Γ Δ) ts
+  helper []       = []
+  helper (t ∷ ts) = addVars t ∷ helper ts
+
+wknMetaAt : ∀ i → Term Σ Γ Δ t → Term Σ Γ (Vec.insert Δ i t′) t
+wknMetaAt′ : ∀ i → All (Term Σ Γ Δ) ts → All (Term Σ Γ (Vec.insert Δ i t′)) ts
+
+wknMetaAt i (state j)   = state j
+wknMetaAt i (var j)     = var j
+wknMetaAt i (meta j)    = castType (meta (Fin.punchIn i j)) (Vecₚ.insert-punchIn _ i _ j)
+wknMetaAt i (func f ts) = func f (wknMetaAt′ i ts)
+
+wknMetaAt′ i []       = []
+wknMetaAt′ i (t ∷ ts) = wknMetaAt i t ∷ wknMetaAt′ i ts
+
+wknMeta : Term Σ Γ Δ t → Term Σ Γ (t′ ∷ Δ) t
+wknMeta = wknMetaAt 0F
+
+wknMeta′ : All (Term Σ Γ Δ) ts → All (Term Σ Γ (t′ ∷ Δ)) ts
+wknMeta′ = wknMetaAt′ 0F
+
+wknMetas : (ts : Vec Type n) → Term Σ Γ Δ t → Term Σ Γ (ts ++ Δ) t
+wknMetas τs (state i)   = state i
+wknMetas τs (var i)     = var i
+wknMetas τs (meta i)    = castType (meta (Fin.raise (Vec.length τs) i)) (Vecₚ.lookup-++ʳ τs _ i)
+wknMetas τs (func f ts) = func f (helper ts)
+  where
+  helper : ∀ {n ts} → All (Term Σ Γ Δ) {n} ts → All (Term Σ Γ (τs ++ Δ)) ts
+  helper []       = []
+  helper (t ∷ ts) = wknMetas τs t ∷ helper ts
+
+func₀ : ⟦ t ⟧ₜ → Term Σ Γ Δ t
+func₀ f = func (λ _ → f) []
+
+func₁ : (⟦ t ⟧ₜ → ⟦ t′ ⟧ₜ) → Term Σ Γ Δ t → Term Σ Γ Δ t′
+func₁ f t = func (λ (x , _) → f x) (t ∷ [])
+
+func₂ : (⟦ t₁ ⟧ₜ → ⟦ t₂ ⟧ₜ → ⟦ t′ ⟧ₜ) → Term Σ Γ Δ t₁ → Term Σ Γ Δ t₂ → Term Σ Γ Δ t′
+func₂ f t₁ t₂ = func (λ (x , y , _) → f x y) (t₁ ∷ t₂ ∷ [])
+
+[_][_≟_] : HasEquality t → Term Σ Γ Δ t → Term Σ Γ Δ t → Term Σ Γ Δ bool
+[ bool ][ t ≟ t′ ] = func₂ (λ (lift x) (lift y) → lift (does (x Bool.≟ y))) t t′
+[ int ][ t ≟ t′ ] = func₂ (λ (lift x) (lift y) → lift (does (x ≟ᶻ y))) t t′
+[ fin ][ t ≟ t′ ] = func₂ (λ (lift x) (lift y) → lift (does (x Fin.≟ y))) t t′
+[ real ][ t ≟ t′ ] = func₂ (λ (lift x) (lift y) → lift (does (x ≟ʳ y))) t t′
+[ bit ][ t ≟ t′ ] = func₂ (λ (lift x) (lift y) → lift (does (x ≟ᵇ₁ y))) t t′
+[ bits ][ t ≟ t′ ] = func₂ (λ xs ys → lift (does (VecF.fromVec (Vec.map lower xs) ≟ᵇ VecF.fromVec (Vec.map lower ys)))) t t′
+
+[_][_<?_] : IsNumeric t → Term Σ Γ Δ t → Term Σ Γ Δ t → Term Σ Γ Δ bool
+[ int ][ t <? t′ ] = func₂ (λ (lift x) (lift y) → lift (does (x <ᶻ? y))) t t′
+[ real ][ t <? t′ ] = func₂ (λ (lift x) (lift y) → lift (does (x <ʳ? y))) t t′
+
+[_][_] : ∀ t → Term Σ Γ Δ (elemType t) → Term Σ Γ Δ (asType t 1)
+[ bits ][ t ] = func₁ (_∷ []) t
+[ array τ ][ t ] = func₁ (_∷ []) t
+
+unbox : ∀ t → Term Σ Γ Δ (asType t 1) → Term Σ Γ Δ (elemType t)
+unbox bits = func₁ Vec.head
+unbox (array t) = func₁ Vec.head
+
+castV : ∀ {a} {A : Set a} {m n} → .(eq : m ≡ n) → Vec A m → Vec A n
+castV {n = 0}     eq []       = []
+castV {n = suc n} eq (x ∷ xs) = x ∷ castV (ℕₚ.suc-injective eq) xs
+
+cast′ : ∀ t → .(eq : m ≡ n) → ⟦ asType t m ⟧ₜ → ⟦ asType t n ⟧ₜ
+cast′ bits      eq = castV eq
+cast′ (array τ) eq = castV eq
+
+cast : ∀ t → .(eq : m ≡ n) → Term Σ Γ Δ (asType t m) → Term Σ Γ Δ (asType t n)
+cast τ eq = func₁ (cast′ τ eq)
+
+[_][-_] : IsNumeric t → Term Σ Γ Δ t → Term Σ Γ Δ t
+[ int ][- t ] = func₁ (lift ∘ ℤ.-_ ∘ lower) t
+[ real ][- t ] = func₁ (lift ∘ ℝ.-_ ∘ lower) t
+
+[_,_,_,_][_+_] : ∀ t₁ t₂ → (isNum₁ : True (isNumeric? t₁)) → (isNum₂ : True (isNumeric? t₂)) → Term Σ Γ Δ t₁ → Term Σ Γ Δ t₂ → Term Σ Γ Δ (combineNumeric t₁ t₂ isNum₁ isNum₂)
+[ int , int , _ , _ ][ t + t′ ] = func₂ (λ (lift x) (lift y) → lift (x ℤ.+ y)) t t′
+[ int , real , _ , _ ][ t + t′ ] = func₂ (λ (lift x) (lift y) → lift (x /1 ℝ.+ y)) t t′
+[ real , int , _ , _ ][ t + t′ ] = func₂ (λ (lift x) (lift y) → lift (x ℝ.+ y /1)) t t′
+[ real , real , _ , _ ][ t + t′ ] = func₂ (λ (lift x) (lift y) → lift (x ℝ.+ y)) t t′
+
+[_,_,_,_][_*_] : ∀ t₁ t₂ → (isNum₁ : True (isNumeric? t₁)) → (isNum₂ : True (isNumeric? t₂)) → Term Σ Γ Δ t₁ → Term Σ Γ Δ t₂ → Term Σ Γ Δ (combineNumeric t₁ t₂ isNum₁ isNum₂)
+[ int , int , _ , _ ][ t * t′ ] = func₂ (λ (lift x) (lift y) → lift (x ℤ.* y)) t t′
+[ int , real , _ , _ ][ t * t′ ] = func₂ (λ (lift x) (lift y) → lift (x /1 ℝ.* y)) t t′
+[ real , int , _ , _ ][ t * t′ ] = func₂ (λ (lift x) (lift y) → lift (x ℝ.* y /1)) t t′
+[ real , real , _ , _ ][ t * t′ ] = func₂ (λ (lift x) (lift y) → lift (x ℝ.* y)) t t′
+
+[_][_^_] : IsNumeric t → Term Σ Γ Δ t → ℕ → Term Σ Γ Δ t
+[ int ][ t ^ n ] = func₁ (lift ∘ (ℤ′._^′ n) ∘ lower) t
+[ real ][ t ^ n ] = func₁ (lift ∘ (ℝ′._^′ n) ∘ lower) t
+
+2≉0 : Set _
+2≉0 = ¬ 2 ℝ′.×′ 1ℝ ℝ.≈ 0ℝ
+
+[_][_>>_] : 2≉0 → Term Σ Γ Δ int → ℕ → Term Σ Γ Δ int
+[ 2≉0 ][ t >> n ] = func₁ (lift ∘ ⌊_⌋ ∘ (ℝ._* 2≉0 ℝ.⁻¹ ℝ′.^′ n) ∘ _/1 ∘ lower) t
+
+-- 0 of y is 0 of result
+join′ : ∀ t → ⟦ asType t m ⟧ₜ → ⟦ asType t n ⟧ₜ → ⟦ asType t (n ℕ.+ m) ⟧ₜ
+join′ bits      = flip _++_
+join′ (array t) = flip _++_
+
+take′ : ∀ t m {n} → ⟦ asType t (m ℕ.+ n) ⟧ₜ → ⟦ asType t m ⟧ₜ
+take′ bits      m = Vec.take m
+take′ (array t) m = Vec.take m
+
+drop′ : ∀ t m {n} → ⟦ asType t (m ℕ.+ n) ⟧ₜ → ⟦ asType t n ⟧ₜ
+drop′ bits      m = Vec.drop m
+drop′ (array t) m = Vec.drop m
+
+private
+  m≤n⇒m+k≡n : ∀ {m n} → m ℕ.≤ n → ∃ λ k → m ℕ.+ k ≡ n
+  m≤n⇒m+k≡n ℕ.z≤n       = _ , refl
+  m≤n⇒m+k≡n (ℕ.s≤s m≤n) = dmap id (cong suc) (m≤n⇒m+k≡n m≤n)
+
+  slicedSize : ∀ n m (i : Fin (suc n)) → ∃ λ k → n ℕ.+ m ≡ Fin.toℕ i ℕ.+ (m ℕ.+ k) × Fin.toℕ i ℕ.+ k ≡ n
+  slicedSize n m i = k , (begin
+    n ℕ.+ m                 ≡˘⟨ cong (ℕ._+ m) (proj₂ i+k≡n) ⟩
+    (Fin.toℕ i ℕ.+ k) ℕ.+ m ≡⟨  ℕₚ.+-assoc (Fin.toℕ i) k m ⟩
+    Fin.toℕ i ℕ.+ (k ℕ.+ m) ≡⟨  cong (Fin.toℕ i ℕ.+_) (ℕₚ.+-comm k m) ⟩
+    Fin.toℕ i ℕ.+ (m ℕ.+ k) ∎) ,
+    proj₂ i+k≡n
+    where
+    open ≡-Reasoning
+    i+k≡n = m≤n⇒m+k≡n (ℕₚ.≤-pred (Finₚ.toℕ<n i))
+    k = proj₁ i+k≡n
+
+-- 0 of x is i of result
+splice′ : ∀ t → ⟦ asType t m ⟧ₜ → ⟦ asType t n ⟧ₜ → ⟦ fin (suc n) ⟧ₜ → ⟦ asType t (n ℕ.+ m) ⟧ₜ
+splice′ {m = m} t x y (lift i) = cast′ t eq (join′ t (join′ t high x) low)
+  where
+  reasoning = slicedSize _ m i
+  k = proj₁ reasoning
+  n≡i+k = sym (proj₂ (proj₂ reasoning))
+  low = take′ t (Fin.toℕ i) (cast′ t n≡i+k y)
+  high = drop′ t (Fin.toℕ i) (cast′ t n≡i+k y)
+  eq = sym (proj₁ (proj₂ reasoning))
+
+splice : ∀ t → Term Σ Γ Δ (asType t m) → Term Σ Γ Δ (asType t n) → Term Σ Γ Δ (fin (suc n)) → Term Σ Γ Δ (asType t (n ℕ.+ m))
+splice τ t₁ t₂ t′ = func (λ (x , y , i , _) → splice′ τ x y i) (t₁ ∷ t₂ ∷ t′ ∷ [])
+
+-- i of x is 0 of first
+cut′ : ∀ t → ⟦ asType t (n ℕ.+ m) ⟧ₜ → ⟦ fin (suc n) ⟧ₜ → ⟦ asType t m ∷ asType t n ∷ [] ⟧ₜ′
+cut′ {m = m} t x (lift i) = middle , cast′ t i+k≡n (join′ t high low) , _
+  where
+  reasoning = slicedSize _ m i
+  k = proj₁ reasoning
+  i+k≡n = proj₂ (proj₂ reasoning)
+  eq = proj₁ (proj₂ reasoning)
+  low = take′ t (Fin.toℕ i) (cast′ t eq x)
+  middle = take′ t m (drop′ t (Fin.toℕ i) (cast′ t eq x))
+  high = drop′ t m (drop′ t (Fin.toℕ i) (cast′ t eq x))
+
+cut : ∀ t → Term Σ Γ Δ (asType t (n ℕ.+ m)) → Term Σ Γ Δ (fin (suc n)) → Term Σ Γ Δ (tuple _ (asType t m ∷ asType t n ∷ []))
+cut τ t t′ = func₂ (cut′ τ) t t′
+
+flatten : ∀ {ms : Vec ℕ n} → ⟦ Vec.map fin ms ⟧ₜ′ → All Fin ms
+flatten {ms = []}     _             = []
+flatten {ms = _ ∷ ms} (lift x , xs) = x ∷ flatten xs
+
+𝒦 : Literal t → Term Σ Γ Δ t
+𝒦 (x ′b) = func₀ (lift x)
+𝒦 (x ′i) = func₀ (lift (x ℤ′.×′ 1ℤ))
+𝒦 (x ′f) = func₀ (lift x)
+𝒦 (x ′r) = func₀ (lift (x ℝ′.×′ 1ℝ))
+𝒦 (x ′x) = func₀ (lift (Bool.if x then 1𝔹 else 0𝔹))
+𝒦 ([] ′xs) = func₀ []
+𝒦 ((x ∷ xs) ′xs) = func₂ (flip Vec._∷ʳ_) (𝒦 (x ′x)) (𝒦 (xs ′xs))
+𝒦 (x ′a) = func₁ Vec.replicate (𝒦 x)
+
+module _ (2≉0 : 2≉0) where
+  ℰ : Code.Expression Σ Γ t → Term Σ Γ Δ t
+  ℰ e = (uncurry helper) (M.elimFunctions e)
+    where
+    1+m⊔n≡1+k : ∀ m n → ∃ λ k → suc m ℕ.⊔ n ≡ suc k
+    1+m⊔n≡1+k m 0       = m , refl
+    1+m⊔n≡1+k m (suc n) = m ℕ.⊔ n , refl
+
+    pull-0₂ : ∀ {x y} → x ℕ.⊔ y ≡ 0 → x ≡ 0
+    pull-0₂ {0} {0}     refl = refl
+    pull-0₂ {0} {suc y} ()
+
+    pull-0₃ : ∀ {x y z} → x ℕ.⊔ y ℕ.⊔ z ≡ 0 → x ≡ 0
+    pull-0₃ {0}     {0}     {0} refl = refl
+    pull-0₃ {0}     {suc y} {0}     ()
+    pull-0₃ {suc x} {0}     {0}     ()
+    pull-0₃ {suc x} {0}     {suc z} ()
+
+    pull-1₃ : ∀ x {y z} → x ℕ.⊔ y ℕ.⊔ z ≡ 0 → y ≡ 0
+    pull-1₃ 0       {0}     {0}     refl = refl
+    pull-1₃ 0       {suc y} {0}     ()
+    pull-1₃ (suc x) {0}     {0}     ()
+    pull-1₃ (suc x) {0}     {suc z} ()
+
+    pull-last : ∀ {x y} → x ℕ.⊔ y ≡ 0 → y ≡ 0
+    pull-last {0}     {0} refl = refl
+    pull-last {suc x} {0} ()
+
+    helper : ∀ (e : Code.Expression Σ Γ t) → M.callDepth e ≡ 0 → Term Σ Γ Δ t
+    helper (Code.lit x) eq = 𝒦 x
+    helper (Code.state i) eq = state i
+    helper (Code.var i) eq = var i
+    helper (Code.abort e) eq = func₁ (λ ()) (helper e eq)
+    helper (Code._≟_ {hasEquality = hasEq} e e₁) eq = [ toWitness hasEq ][ helper e (pull-0₂ eq) ≟ helper e₁ (pull-last eq) ]
+    helper (Code._<?_ {isNumeric = isNum} e e₁) eq = [ toWitness isNum ][ helper e (pull-0₂ eq) <? helper e₁ (pull-last eq) ]
+    helper (Code.inv e) eq = func₁ (lift ∘ Bool.not ∘ lower) (helper e eq)
+    helper (e Code.&& e₁) eq = func₂ (λ (lift x) (lift y) → lift (x Bool.∧ y)) (helper e (pull-0₂ eq)) (helper e₁ (pull-last eq))
+    helper (e Code.|| e₁) eq = func₂ (λ (lift x) (lift y) → lift (x Bool.∨ y)) (helper e (pull-0₂ eq)) (helper e₁ (pull-last eq))
+    helper (Code.not e) eq = func₁ (Vec.map (lift ∘ 𝔹.¬_ ∘ lower)) (helper e eq)
+    helper (e Code.and e₁) eq = func₂ (λ xs ys → Vec.zipWith (λ (lift x) (lift y) → lift (x 𝔹.∧ y)) xs ys) (helper e (pull-0₂ eq)) (helper e₁ (pull-last eq))
+    helper (e Code.or e₁) eq = func₂ (λ xs ys → Vec.zipWith (λ (lift x) (lift y) → lift (x 𝔹.∨ y)) xs ys) (helper e (pull-0₂ eq)) (helper e₁ (pull-last eq))
+    helper (Code.[_] {t = t} e) eq = [ t ][ helper e eq ]
+    helper (Code.unbox {t = t} e) eq = unbox t (helper e eq)
+    helper (Code.splice {t = t} e e₁ e₂) eq = splice t (helper e (pull-0₃ eq)) (helper e₁ (pull-1₃ (M.callDepth e) eq)) (helper e₂ (pull-last eq))
+    helper (Code.cut {t = t} e e₁) eq = cut t (helper e (pull-0₂ eq)) (helper e₁ (pull-last eq))
+    helper (Code.cast {t = t} i≡j e) eq = cast t i≡j (helper e eq)
+    helper (Code.-_ {isNumeric = isNum} e) eq = [ toWitness isNum ][- helper e eq ]
+    helper (Code._+_ {isNumeric₁ = isNum₁} {isNumeric₂ = isNum₂} e e₁) eq = [ _ , _ , isNum₁ , isNum₂ ][ helper e (pull-0₂ eq) + helper e₁ (pull-last eq) ]
+    helper (Code._*_ {isNumeric₁ = isNum₁} {isNumeric₂ = isNum₂} e e₁) eq = [ _ , _ , isNum₁ , isNum₂ ][ helper e (pull-0₂ eq) * helper e₁ (pull-last eq) ]
+    helper (Code._^_ {isNumeric = isNum} e y) eq = [ toWitness isNum ][ helper e eq ^ y ]
+    helper (e Code.>> n) eq = [ 2≉0 ][ helper e eq >> n ]
+    helper (Code.rnd e) eq = func₁ (lift ∘ ⌊_⌋ ∘ lower) (helper e eq)
+    helper (Code.fin f e) eq = func₁ (lift ∘ f ∘ flatten) (helper e eq)
+    helper (Code.asInt e) eq = func₁ (lift ∘ (ℤ′._×′ 1ℤ) ∘ Fin.toℕ ∘ lower) (helper e eq)
+    helper Code.nil eq = func₀ _
+    helper (Code.cons e e₁) eq = func₂ _,_ (helper e (pull-0₂ eq)) (helper e₁ (pull-last eq))
+    helper (Code.head e) eq = func₁ proj₁ (helper e eq)
+    helper (Code.tail e) eq = func₁ proj₂ (helper e eq)
+    helper (Code.call f es) eq = contradiction (trans (sym eq) (proj₂ (1+m⊔n≡1+k (M.funCallDepth f) (M.callDepth′ es)))) ℕₚ.0≢1+n
+    helper (Code.if e then e₁ else e₂) eq = func (λ (lift b , x , x₁ , _) → Bool.if b then x else x₁) (helper e (pull-0₃ eq) ∷ helper e₁ (pull-1₃ (M.callDepth e) eq) ∷ helper e₂ (pull-last eq) ∷ [])
+
+  ℰ′ : All (Code.Expression Σ Γ) ts → All (Term Σ Γ Δ) ts
+  ℰ′ []       = []
+  ℰ′ (e ∷ es) = ℰ e ∷ ℰ′ es
+
+  subst : Term Σ Γ Δ t → {e : Code.Expression Σ Γ t′} → Code.CanAssign Σ e → Term Σ Γ Δ t′ → Term Σ Γ Δ t
+  subst t (Code.state i) t′ = substState t i t′
+  subst t (Code.var i) t′ = substVar t i t′
+  subst t (Code.abort e) t′ = func₁ (λ ()) (ℰ e)
+  subst t (Code.[_] {t = τ} ref) t′ = subst t ref (unbox τ t′)
+  subst t (Code.unbox {t = τ} ref) t′ = subst t ref [ τ ][ t′ ]
+  subst t (Code.splice {t = τ} ref ref₁ e₃) t′ = subst (subst t ref (func₁ proj₁ (cut τ t′ (ℰ e₃)))) ref₁ (func₁ (proj₁ ∘ proj₂) (cut τ t′ (ℰ e₃)))
+  subst t (Code.cut {t = τ} ref e₂) t′ = subst t ref (splice τ (func₁ proj₁ t′) (func₁ (proj₁ ∘ proj₂) t′) (ℰ e₂))
+  subst t (Code.cast {t = τ} eq ref) t′ = subst t ref (cast τ (sym eq) t′)
+  subst t Code.nil t′ = t
+  subst t (Code.cons ref ref₁) t′ = subst (subst t ref (func₁ proj₁ t′)) ref₁ (func₁ proj₂ t′)
+  subst t (Code.head {e = e} ref) t′ = subst t ref (func₂ _,_ t′ (func₁ proj₂ (ℰ e)))
+  subst t (Code.tail {t = τ} {e = e} ref) t′ = subst t ref (func₂ {t₁ = τ} _,_ (func₁ proj₁ (ℰ e)) t′)
+
+⟦_⟧ : Term Σ Γ Δ t → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ Δ ⟧ₜ′ → ⟦ t ⟧ₜ
+⟦_⟧′ : ∀ {ts} → All (Term Σ Γ Δ) {n} ts → ⟦ Σ ⟧ₜ′ → ⟦ Γ ⟧ₜ′ → ⟦ Δ ⟧ₜ′ → ⟦ ts ⟧ₜ′
+
+⟦ state i ⟧ σ γ δ = fetch i σ
+⟦ var i ⟧ σ γ δ = fetch i γ
+⟦ meta i ⟧ σ γ δ = fetch i δ
+⟦ func f ts ⟧ σ γ δ = f (⟦ ts ⟧′ σ γ δ)
+
+⟦ [] ⟧′     σ γ δ = _
+⟦ t ∷ ts ⟧′ σ γ δ = ⟦ t ⟧ σ γ δ , ⟦ ts ⟧′ σ γ δ
diff --git a/src/Helium/Semantics/Axiomatic/Triple.agda b/src/Helium/Semantics/Axiomatic/Triple.agda
new file mode 100644
index 0000000..7564983
--- /dev/null
+++ b/src/Helium/Semantics/Axiomatic/Triple.agda
@@ -0,0 +1,46 @@
+------------------------------------------------------------------------
+-- Agda Helium
+--
+-- Definition of Hoare triples
+------------------------------------------------------------------------
+
+{-# OPTIONS --safe --without-K #-}
+
+open import Helium.Data.Pseudocode.Types using (RawPseudocode)
+
+module Helium.Semantics.Axiomatic.Triple
+  {b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃}
+  (rawPseudocode : RawPseudocode b₁ b₂ i₁ i₂ i₃ r₁ r₂ r₃)
+  where
+
+private
+  open module C = RawPseudocode rawPseudocode
+
+import Data.Bool as Bool
+import Data.Fin as Fin
+open import Data.Fin.Patterns
+open import Data.Nat using (suc)
+open import Data.Vec using (Vec; _∷_)
+open import Function using (_∘_)
+open import Helium.Data.Pseudocode.Core
+open import Helium.Semantics.Axiomatic.Assertion rawPseudocode as Asrt
+open import Helium.Semantics.Axiomatic.Term rawPseudocode as Term using (var; meta; func₀; func₁; 𝒦; ℰ; ℰ′)
+open import Level using (_⊔_; lift; lower) renaming (suc to ℓsuc)
+open import Relation.Nullary.Decidable.Core using (toWitness)
+open import Relation.Unary using (_⊆′_)
+
+module _ (2≉0 : Term.2≉0) {o} {Σ : Vec Type o} where
+  open Code Σ
+  data HoareTriple {n} {Γ : Vec Type n} {m} {Δ : Vec Type m} : Assertion Σ Γ Δ → Statement Γ → Assertion Σ Γ Δ → Set (ℓsuc (b₁ ⊔ i₁ ⊔ r₁)) where
+    _∙_ : ∀ {P Q R s₁ s₂} → HoareTriple P s₁ Q → HoareTriple Q s₂ R → HoareTriple P (s₁ ∙ s₂) R
+    skip : ∀ {P} → HoareTriple P skip P
+
+    assign : ∀ {P t ref canAssign e} → HoareTriple (subst 2≉0 P (toWitness canAssign) (ℰ 2≉0 e)) (_≔_ {t = t} ref {canAssign} e) P
+    declare : ∀ {t P Q e s} → HoareTriple (P ∧ equal (var 0F) (Term.wknVar (ℰ 2≉0 e))) s (Asrt.wknVar Q) → HoareTriple (Asrt.elimVar P (ℰ 2≉0 e)) (declare {t = t} e s) Q
+    invoke : ∀ {m ts P Q s es} → HoareTriple P s (Asrt.addVars Q) → HoareTriple (Asrt.substVars P (ℰ′ 2≉0 es)) (invoke {m = m} {ts} (s ∙end) es) (Asrt.addVars Q)
+    if : ∀ {P Q e s} → HoareTriple (P ∧ equal (ℰ 2≉0 e) (𝒦 (Bool.true ′b))) s Q → HoareTriple (P ∧ equal (ℰ 2≉0 e) (𝒦 (Bool.false ′b))) skip Q → HoareTriple P (if e then s) Q
+    if-else : ∀ {P Q e s₁ s₂} → HoareTriple (P ∧ equal (ℰ 2≉0 e) (𝒦 (Bool.true ′b))) s₁ Q → HoareTriple (P ∧ equal (ℰ 2≉0 e) (𝒦 (Bool.false ′b))) s₂ Q → HoareTriple P (if e then s₁ else s₂) Q
+    for : ∀ {m} {I : Assertion Σ Γ (fin (suc m) ∷ Δ)} {s} → HoareTriple (some (Asrt.wknVar (Asrt.wknMetaAt 1F I) ∧ equal (meta 1F) (var 0F) ∧ equal (meta 0F) (func₁ (lift ∘ Fin.inject₁ ∘ lower) (meta 1F)))) s (some (Asrt.wknVar (Asrt.wknMetaAt 1F I) ∧ equal (meta 0F) (func₁ (lift ∘ Fin.suc ∘ lower) (meta 1F)))) → HoareTriple (some (I ∧ equal (meta 0F) (func₀ (lift 0F)))) (for m s) (some (I ∧ equal (meta 0F) (func₀ (lift (Fin.fromℕ m)))))
+
+    consequence : ∀ {P₁ P₂ Q₁ Q₂ s} → (∀ σ γ δ → ⟦ P₁ ⟧ σ γ δ → ⟦ P₂ ⟧ σ γ δ) → HoareTriple P₂ s Q₂ → (∀ σ γ δ → ⟦ Q₂ ⟧ σ γ δ → ⟦ Q₁ ⟧ σ γ δ) → HoareTriple P₁ s Q₁
+    some : ∀ {t P Q s} → HoareTriple P s Q → HoareTriple (some {t = t} P) s (some Q)