diff --git a/LeanBoogie/Boogie.lean b/LeanBoogie/Boogie.lean
index f896555..e96e978 100644
--- a/LeanBoogie/Boogie.lean
+++ b/LeanBoogie/Boogie.lean
@@ -55,7 +55,7 @@ abbrev Boogie.bind : (Boogie A) -> (A -> Boogie B) -> Boogie B := Bind.bind
 def Boogie.run (m : Boogie Unit) (fuel : Nat) : Option BoogieState :=
   let s₀ : BoogieState := (fun _ => 0)
   let stuff := StateT.run m s₀
-  let ⟨_, ret⟩ := ITree.run stuff Empty.elim fuel
+  let ⟨_, ret⟩ := runLog stuff Empty.elim fuel
   ret.map Prod.snd
 
 theorem Boogie.ite_push_state [Decidable c] {t e : Boogie A}
diff --git a/LeanBoogie/Experimental/State.lean b/LeanBoogie/Experimental/State.lean
index 03877d3..c6920cc 100644
--- a/LeanBoogie/Experimental/State.lean
+++ b/LeanBoogie/Experimental/State.lean
@@ -37,18 +37,62 @@ def ConA : Con -> Type
 instance : CoeSort Ty Type := ⟨TyA⟩
 instance : CoeSort Con Type := ⟨ConA⟩
 
+set_option linter.unusedVariables false in
+def ConA.get : {Γ : Con} -> Γ -> Var Γ A -> A
+| _ :: _, (x, _), .vz   => x
+| _ :: _, (_, γ), .vs v => γ.get v
+
+set_option linter.unusedVariables false in
+def ConA.update : {Γ : Con} -> Γ -> Var Γ A -> A -> Γ
+| _ :: _, (_, γ), .vz  , a' => (a', γ)
+| _ :: _, (a, γ), .vs v, a' => (a, γ.update v a')
+
+/- ### Normal form of `ConA`
+  Given a starting `γ : ConA Γ` and `γ' = γ.update |>.update .. |>.update ... |> ...`,
+  we can normalize these into essentially `γ' = { #0 := ...γ..., #1 := ...γ..., #2 := ...γ..., ...}`
+  We should have a tactic which performs this normalization in a performant way.
+-/
+@[simp] theorem ConA.update_lww {Γ : Con} {v : Var Γ A} {γ : Γ} : (γ.update v a').update v a'' = γ.update v a'' := sorry
+@[simp] theorem ConA.update_get {Γ : Con} {v : Var Γ A} {γ : Γ} : (γ.update v a').get v = a' := by
+  induction Γ with
+  | nil => cases v
+  | cons B Γ ih =>
+    cases v with
+    | vz => rfl
+    | vs v => simp only [get, ih]
+-- more theorems
+
 -- ## Interaction Tree Events for State
 
-namespace Approach1
-  inductive Mem (Γ : Con) : /- Type -> -/ Type where
-  | rd : Var Γ A          -> Mem Γ /- (TyA A) -/
-  | wr : Var Γ A -> TyA A -> Mem Γ /- Unit -/
-  -- def Mem.read  (v : Var Γ A)           : ITree (Mem Γ) A := .vis (.rd v) (fun a:A => .ret a)
-  -- def Mem.write (v : Var Γ A) (val : A) : ITree (Mem Γ) A := .vis (.wr v val) (fun () => .ret ())
-end Approach1
-
-namespace Approach2
-  inductive Mem (Γ : Type) : /- (A:Type) -> -/ Type where
-  | rd (π : Γ -> Ans) : Mem Γ /- A -/
-  | wr (δ : Γ -> Ans -> Γ) : Mem Γ /- Unit -/
-end Approach2
+inductive Mem (Γ : Con) : Type -> Type where
+| rd : Var Γ A          -> Mem Γ A
+| wr : Var Γ A -> TyA A -> Mem Γ Unit
+
+def Mem.read  (v : Var Γ A)           : ITree (Mem Γ) A    := .vis (.rd v    ) (fun (a : A) => .ret a)
+def Mem.write (v : Var Γ A) (val : A) : ITree (Mem Γ) Unit := .vis (.wr v val) (fun () => .ret ())
+
+-- ## Example:
+
+structure Global_ where
+  i : Int
+  n : BitVec 32
+
+def Global.Γ : Con := [.int, .bv 32]
+abbrev Global : Type := Global.Γ
+abbrev Global.i (γ : Global) : Int       := γ.get .vz
+abbrev Global.n (γ : Global) : BitVec 32 := γ.get (.vs .vz)
+
+#check Global_.i
+#check Global.i
+
+def Empty' : Type -> Type := fun _ => Empty
+
+inductive Plus (E₁ E₂ : Type -> Type) : Type -> Type
+| left  : E₁ X -> Plus E₁ E₂ X
+| right : E₂ X -> Plus E₁ E₂ X
+
+instance : HAdd (Type -> Type) (Type -> Type) (Type -> Type) := ⟨Plus⟩
+
+def merge : ITree (Mem Γ + Mem Δ) A -> ITree (Mem (Γ ++ Δ)) A := sorry
+
+def interp : ITree (Mem Γ) Unit -> StateT (ConA Γ) (ITree Empty') Unit := sorry
diff --git a/LeanBoogie/ITree/Eutt.lean b/LeanBoogie/ITree/Eutt.lean
index 6a90cee..fd3eb88 100644
--- a/LeanBoogie/ITree/Eutt.lean
+++ b/LeanBoogie/ITree/Eutt.lean
@@ -57,7 +57,7 @@ instance ITree.setoid : Setoid (ITree E A) where
   r := Eutt
   iseqv := ⟨Eutt.refl, Eutt.symm, Eutt.trans⟩
 
-instance Internal.ITree.setoid : Setoid (Internal.ITree Ans E A) := _root_.ITree.setoid -- typeclass resolution isn't able to figure this out on its own...
+instance Internal.ITree.setoid : Setoid (ITree E A) := _root_.ITree.setoid -- typeclass resolution isn't able to figure this out on its own...
 
 theorem Eutt.ret : @ITree.ret E A r ≈ .ret r := Eutt.refl _
 
diff --git a/LeanBoogie/ITree/Events.lean b/LeanBoogie/ITree/Events.lean
new file mode 100644
index 0000000..1062720
--- /dev/null
+++ b/LeanBoogie/ITree/Events.lean
@@ -0,0 +1,18 @@
+import LeanBoogie.ITree.ITree
+
+namespace ITree
+
+/-
+  # Events
+-/
+
+instance (priority := low) : OfNat (Type -> Type) n where ofNat := fun _ => Fin n
+instance : OfNat (Type -> Type) 0 where ofNat := fun _ => PEmpty
+instance : OfNat (Type -> Type) 1 where ofNat := fun _ => PUnit
+
+/-- The union of two event types. -/
+inductive EvProd (E₁ E₂ : Type -> Type) : Type -> Type
+| left  : E₁ X -> EvProd E₁ E₂ X
+| right : E₂ X -> EvProd E₁ E₂ X
+
+instance : HAdd (Type -> Type) (Type -> Type) (Type -> Type) := ⟨EvProd⟩
diff --git a/LeanBoogie/ITree/Examples.lean b/LeanBoogie/ITree/Examples.lean
index 72721e1..a1ed216 100644
--- a/LeanBoogie/ITree/Examples.lean
+++ b/LeanBoogie/ITree/Examples.lean
@@ -1,9 +1,11 @@
 import Qpf
 import LeanBoogie.ITree.ITree
 import LeanBoogie.ITree.Eutt
+import LeanBoogie.ITree.Events
 
 open MvQPF
 open ITree
+
 instance : Repr Empty where reprPrec _ _ := ""
 
 inductive Ev : Type
@@ -11,9 +13,6 @@ inductive Ev : Type
 | output : Int -> Ev -- We would really like this to be `-> Ev Unit`, but can't due to the `(A : Type) -> ...` QPF issue.
 deriving Repr
 
-/-- Spin forever. -/
-def spin : ITree Empty Empty := ITree.corec (fun n => .tau n) 0
-
 /-- Just echo once. -/
 def echo1 : ITree Ev Unit :=
   .vis .input fun (answer : Int) =>
diff --git a/LeanBoogie/ITree/ITree.lean b/LeanBoogie/ITree/ITree.lean
index 7030bcd..9418add 100644
--- a/LeanBoogie/ITree/ITree.lean
+++ b/LeanBoogie/ITree/ITree.lean
@@ -1,6 +1,8 @@
 import Qpf
 import Mathlib.Data.QPF.Multivariate.Constructions.Sigma
 
+namespace ITree
+
 /-!
 # Interaction Trees
 
@@ -13,7 +15,6 @@ semantics of side-effecting, possibly non-terminating, programs
 Thank you to Alex Keizer (github.com/alexkeizer) for the help in figuring this out!
 -/
 
-namespace ITree
 
 /-
   ## Step 1: Defining Shape
@@ -201,6 +202,10 @@ abbrev vis {E : Type -> Type} {A : Type} {Ans : Type} (e : E Ans) (k : Ans -> IT
 def corec {E : Type -> Type} {A : Type} {β : Type 1} (f : β → Base E A β) (b : β) : ITree E A
   := MvQPF.Cofix.corec (n := 1) (F := Base.Uncurried E) f b
 
+def dest {E : Type -> Type} {A : Type} : ITree E A -> Base E A (ITree E A)
+  := MvQPF.Cofix.dest
+
+@[cases_eliminator, elab_as_elim]
 def cases {E : Type -> Type} {A : Type} {motive : ITree E A -> Sort u}
   (ret : (r : A) → motive (ret r))
   (tau : (x : ITree E A) → motive (tau x))
@@ -222,3 +227,34 @@ def cases {E : Type -> Type} {A : Type} {motive : ITree E A -> Sort u}
       apply_fun MvQPF.Cofix.mk at h
       simpa [MvQPF.Cofix.mk_dest] using h
     h ▸ vis e (fun ans => k (.up ans))
+
+-- Computation rules
+theorem cases_ret : cases (motive := motive) c_ret c_tau c_vis (.ret r) = c_ret r := rfl
+theorem cases_tau : cases (motive := motive) c_ret c_tau c_vis (.tau t) = c_tau t := sorry
+theorem cases_vis : cases (motive := motive) c_ret c_tau c_vis (.vis e k) = c_vis e k := sorry
+
+
+/-
+  # Some common stuff
+-/
+
+def spin : ITree E A := corec (fun .unit => .tau .unit) PUnit.unit
+
+
+/-- Just a convenience function. Re-plays a tree within another tree. -/
+def Base.replay (ta : ITree E A₁) (fTree : ITree E A₁ -> C) (fRet : A₁ -> A₂ := by exact id) : ITree.Base E A₂ C := sorry
+--   match ta.dest with
+--   | .ret (.up a : _) => .ret (.up (fRet a))
+--   | .tau (t : ITree E A₁) => .tau (fTree t)
+--   | .vis ⟨_, e, k⟩ => .vis e (fun x => fTree (k x))
+
+def _root_.TypeVec.ofList : (l : List Type) -> TypeVec l.length
+| [] => Vec.nil
+| t :: l => TypeVec.ofList l |>.append1 t
+
+def Base.Map (f : C -> D) : TypeVec.Arrow (TypeVec.ofList [C, B, E]) (TypeVec.ofList [D, B, E])
+  := TypeVec.appendFun TypeVec.id f
+
+-- TODO:
+-- def Base.Inr : TypeVec.Arrow (TypeVec.ofList [ITree E B, B, E]) (TypeVec.ofList [ITree E A ⊕ ITree E B, B, E])
+--   := TypeVec.appendFun TypeVec.id Sum.inr
diff --git a/LeanBoogie/ITree/Imp.lean b/LeanBoogie/ITree/Imp.lean
index 0807d21..3613e1e 100644
--- a/LeanBoogie/ITree/Imp.lean
+++ b/LeanBoogie/ITree/Imp.lean
@@ -1,4 +1,6 @@
 import LeanBoogie.ITree.ITree
+import LeanBoogie.ITree.Monad
+import LeanBoogie.ITree.Iter
 import LeanBoogie.ITree.Eutt
 import LeanBoogie.Notation
 import LeanBoogie.Iter
@@ -10,7 +12,7 @@ namespace ITree
 def skip : ITree E Unit := Pure.pure ()
 def seq (a b : ITree E Unit) : ITree E Unit := Bind.bind a (fun () => b)
 instance : Seqi (ITree E Unit) := ⟨ITree.seq⟩
-def trigger (e : E) : ITree E Int := .vis e .ret
+-- def trigger (e : E Ans) : ITree E Int := .vis e .ret
 def ite (c : ITree E Bool) (t e : ITree E A) : ITree E A := Bind.bind c (fun c => if c then t else e)
 abbrev ifthen (c : ITree E Bool) (t : ITree E Unit) : ITree E Unit := ite c t skip
 
diff --git a/LeanBoogie/ITree/Iter.lean b/LeanBoogie/ITree/Iter.lean
new file mode 100644
index 0000000..b9517a9
--- /dev/null
+++ b/LeanBoogie/ITree/Iter.lean
@@ -0,0 +1,60 @@
+import LeanBoogie.ITree.ITree
+import LeanBoogie.ITree.Monad
+
+namespace ITree
+
+/-
+  ## ITrees form an *iterative* monad
+-/
+
+
+/-- Repeat a computation until it returns `B`.
+
+  From the ITrees paper, page 12:
+  ```
+  CoFixpoint iter (body : A → itree E (A + B)) : A → itree E B :=
+    fun a ⇒ ab <- body a ;;
+      match ab with
+      | inl a ⇒ Tau (iter body a)
+      | inr b ⇒ Ret b
+      end.
+  ``` -/
+def iter (body : A -> ITree E (A ⊕ B)) (a₀ : A) : ITree E B := sorry -- TODO
+  -- ITree.corec (fun (x : A ⊕ ITree E (B)) =>
+  --   match x with
+  --   | .inl a =>
+  --     -- Run the body, if it returned `a` we iter again, if it returned `b` we are done.
+  --     let res : ITree E (A ⊕ B) := bind (body a) (fun ab =>
+  --       match ab with
+  --       | .inl a => .ret (.inl a)
+  --       | .inr b => .ret (.inr b)
+  --     )
+  --     match res.dest with
+  --     -- | .ret (a : A ⊕ B) => .ret sorry
+  --     | .ret (.inl a) => .tau (.inl a) -- call `iter body a`
+  --     | .ret (.inr b) => .ret b -- we are done
+  --     | .tau (t : ITree E _) => .tau (.inr t)
+  --     | .vis e k => sorry
+  --   | .inr b => Base.replay b .inr
+  -- ) (Sum.inl a₀)
+
+theorem iter_fp {f : A -> ITree E (A ⊕ B)}
+  : iter f a₀ = do let ab <- f a₀
+                   match ab with
+                   | .inl a => (iter f a)
+                   | .inr b => return b
+  := by sorry
+
+/--
+  Definition loop (body : C + A → itree E (C + B)) : A → itree E B :=
+    fun a ⇒ iter (fun ca ⇒
+      cb <- body ca ;;
+      match cb with
+      | inl c ⇒ Ret (inl (inl c))
+      | inr b ⇒ Ret (inr b)
+      end) (inr a).
+-/
+def loop (body : Sum C A -> ITree E (Sum C B)) (a : A) : ITree E B := sorry
+
+def iter_lift (body : A -> ITree E (A ⊕ B)) : (A ⊕ B) -> ITree E (A ⊕ B) :=
+  fun | .inl a => body a | .inr b => return .inr b
diff --git a/LeanBoogie/ITree/Monad.lean b/LeanBoogie/ITree/Monad.lean
new file mode 100644
index 0000000..6babbf3
--- /dev/null
+++ b/LeanBoogie/ITree/Monad.lean
@@ -0,0 +1,42 @@
+import LeanBoogie.ITree.ITree
+
+namespace ITree
+
+/-
+  # ITrees form a monad
+-/
+
+def pure (a : A) : ITree E A := .ret a
+
+def bind (ta : ITree E A) (tb : A -> ITree E B) : ITree E B := sorry -- TODO: fix
+  -- ITree.corec (β := Sum (ITree E A) (ITree E B)) (fun x =>
+  --   match x with
+  --   | .inl ta =>
+  --     match ta.dest with
+  --     | .ret (.up a : ULift A) =>
+  --       let tb : ITree E B := tb a
+  --       let ret : ITree.Base E B (ITree E B) := tb.dest
+  --       let ret : ITree.Base E B (ITree E A ⊕ ITree E B) := MvFunctor.map (F := TypeFun.ofCurried (n := _) Base) Base.Inr ret
+  --       ret
+  --     | .tau t => .tau (.inl t)
+  --     | .vis e k => .vis e (fun x => .inl (k x))
+  --   | .inr b => Base.replay b Sum.inr
+  -- ) (Sum.inl ta)
+
+instance : Monad (ITree E) where
+  pure := pure
+  bind := bind
+
+instance : LawfulFunctor (ITree E) where
+  map_const := sorry
+  id_map := sorry
+  comp_map := sorry
+
+instance : LawfulMonad (ITree E) where
+  seqLeft_eq := sorry
+  seqRight_eq := sorry
+  pure_seq := sorry
+  bind_pure_comp := sorry
+  bind_map := sorry
+  pure_bind := sorry
+  bind_assoc := sorry
diff --git a/LeanBoogie/ITree/QITree.lean b/LeanBoogie/ITree/QITree.lean
index 904213a..8556d62 100644
--- a/LeanBoogie/ITree/QITree.lean
+++ b/LeanBoogie/ITree/QITree.lean
@@ -5,7 +5,7 @@ import Mathlib.Data.Quot
   # Quotient of ITree along Eutt
 -/
 
-def QITree (E A : Type) : Type := Quotient (α := ITree E A) ITree.setoid
+def QITree (E : Type -> Type) (A : Type) : Type 1 := Quotient (α := ITree E A) ITree.setoid
 def QITree.ret (a : A) : QITree E A := Quotient.mk ITree.setoid (ITree.ret a)
 def QITree.tau (t : QITree E A) : QITree E A := Quotient.liftOn t (⟦ITree.tau ·⟧) (by
   intro t t' h
@@ -14,11 +14,11 @@ def QITree.tau (t : QITree E A) : QITree E A := Quotient.liftOn t (⟦ITree.tau
   exact Quotient.sound this
 )
 
-opaque QITree.vis_impl (e : E) (k : Ans -> QITree E A) : QITree E A := sorry
+opaque QITree.vis_impl (e : E Ans) (k : Ans -> QITree E A) : QITree E A := sorry
 
 -- https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Quot.20lifting.20.60.28_.20-.3E.20T.29.20-.3E.20T.60.20to.20.60.28_.20-.3E.20Q.29.20-.3E.20Q.60/near/484606314
 @[implemented_by QITree.vis_impl]
-def QITree.vis (e : E) (k : Ans -> QITree E A) : QITree E A :=
+def QITree.vis (e : E Ans) (k : Ans -> QITree E A) : QITree E A :=
   Quotient.liftOn (Quotient.choice k) (⟦ITree.vis e ·⟧) (fun _ _ => Quotient.eq.mpr ∘ Eutt.vis)
 
 #check Quot.lift
@@ -31,10 +31,10 @@ example (t : QITree E A) : QITree.tau t = t := by
   sorry
 
 set_option pp.proofs true in
-def QITree.cases {E A : Type} {motive : QITree E A → Sort u}
+def QITree.cases {E : Type -> Type} {A : Type} {motive : QITree E A → Sort u}
     (c_ret : (r : A) → motive (.ret r))
     (c_tau : (x : QITree E A) → motive (.tau x))
-    (c_vis : (e : E) → (k : Ans → QITree E A) → motive (.vis e k))
+    (c_vis : {Ans : Type} -> (e : E Ans) → (k : Ans → QITree E A) → motive (.vis e k))
     (x : QITree E A)
     : motive x
     := Quotient.recOn x
@@ -78,13 +78,13 @@ def QITree.cases {E A : Type} {motive : QITree E A → Sort u}
       )
 
 set_option pp.proofs true in
-def QITree.cases_2 {E A : Type} {motive : QITree E A → Sort u}
+def QITree.cases_2 {A : Type} {motive : QITree E A → Sort u}
   (c_ret : (r : A) → motive (.ret r))
   -- (tau : (x : QITree E A) → motive (.tau x)) -- // Note: Even with quotients we can't get rid of this case. Imagine `QITree.cases (motive := False when .tau) c_ret c_vis spin : False`. Or... maybe this is okay, because we can not write that motive type in the first place, since we can't distinguish between `.ret : QITree` and `.tau _ : QITree`.
-  (c_vis : (e : E) → (k : Ans → QITree E A) → motive (.vis e k))
+  (c_vis : (e : E Ans) → (k : Ans → QITree E A) → motive (.vis e k))
   (x : QITree E A)
   : motive x
-  := Quotient.liftOn₂ (Quotient.choice)
+  := sorry -- ? Quotient.liftOn₂ (Quotient.choice)
 
 
 
diff --git a/LeanBoogie/ITree/RunFinite.lean b/LeanBoogie/ITree/RunFinite.lean
new file mode 100644
index 0000000..0d69d8c
--- /dev/null
+++ b/LeanBoogie/ITree/RunFinite.lean
@@ -0,0 +1,29 @@
+import LeanBoogie.ITree.ITree
+import LeanBoogie.ITree.Monad
+
+namespace ITree
+
+/-- Execute a finite amount of steps of a potentially infinite
+  Returns the events encountered along the way (if any), and the final state (if any).
+  Uses `f` to determine the answer to events. -/
+def runLog (t : ITree E A) (f : ∀Ans, E Ans -> Ans) : Nat -> (List ((Ans : Type) × E Ans)) × Option A
+| 0 => ([], none)
+| n+1 => match t.dest with
+  | .ret (.up a) => ([], some a)
+  | .tau t => runLog t f n
+  | .vis ⟨Ans, .up e, k⟩ => by
+    let t : ITree E A := k (.up (f _ e))
+    let (evs, ret) := runLog t f n
+    exact (⟨Ans, e⟩ :: evs, ret)
+
+/-- Run at most `fuel` steps of `t` in a monad, calling `f` for every event. -/
+def run [Monad m] (t : ITree E A) (fuel : Nat) (f : ∀{Ans}, E Ans -> m Ans) : m (Option A) :=
+  match fuel with
+  | 0 => return none
+  | fuel+1 => match t.dest with
+    | .ret (.up a) => return a
+    | .tau t => run t fuel f
+    | .vis ⟨_, .up e, k⟩ => do
+      let ans <- f e
+      let t : ITree E A := k (.up ans)
+      run t fuel f
diff --git a/LeanBoogie/Notation.lean b/LeanBoogie/Notation.lean
index 0c36316..c6103ba 100644
--- a/LeanBoogie/Notation.lean
+++ b/LeanBoogie/Notation.lean
@@ -1,20 +1,20 @@
 
 /-- Two imperative programs executed after one another. Provides the `;; ` notation. -/
-class Seqi (A : Type) where
+class Seqi (A : Type u) where
   seqi : A -> A -> A
 infixl:20 ";; " => Seqi.seqi
 
 /-- Concatenation of continuations. Provides the `>>>` notation. -/
-class Cat (K : Type -> Type -> Type) where
+class Cat (K : Type u -> Type u -> Type u) where
   cat : K A B -> K B C -> K A C
 infixl:75 " >>> " => Cat.cat
 
 /-- Monad morphism from a computation monad `M` to a specification monad `W`. -/
-class Theta (M : Type -> Type) (W : outParam (Type -> Type)) where
+class Theta (M : Type u -> Type u) (W : outParam (Type u -> Type u)) where
   θ : M A -> W A
 export Theta (θ)
 
-class LawfulTheta (M : (Type -> Type)) [m : Monad M] (W : outParam (Type -> Type)) [w : Monad W] [Theta M W] : Prop where
+class LawfulTheta (M : (Type u -> Type u)) [m : Monad M] (W : outParam (Type u -> Type u)) [w : Monad W] [Theta M W] : Prop where
   θ_pure : θ (m.pure a) = w.pure a
   θ_bind : θ (m.bind a b) = w.bind (θ a) (fun a => θ (b a))