diff --git a/ITree/Basic.lean b/ITree/Basic.lean
index 20edf44..4d99aea 100644
--- a/ITree/Basic.lean
+++ b/ITree/Basic.lean
@@ -36,10 +36,10 @@ Unfortunately, this, too yields an error, so for now we settle for fixing a
 particular input type `α`, by making `α` a parameter of the type.
 -/
 
-codata ITree α ε ρ where
+codata ITree (α : Type) ε ρ where
   | ret (r : ρ)
   | tau (t : ITree α ε ρ)
-  | vis : ε → α → ITree α ε ρ → ITree α ε ρ
+  | vis : ε → (α → ITree α ε ρ) → ITree α ε ρ
 
 
 namespace ITree
@@ -48,10 +48,98 @@ namespace ITree
 cotree, as being generated by some transition function `f`
 from initial state `b` -/
 def corec {β α ε ρ : Type} (f : β → ITree.Base α ε ρ β) (b : β) : ITree α ε ρ :=
-  MvQPF.Cofix.corec (F := TypeFun.ofCurried ITree.Base) f b
+  MvQPF.Cofix.corec (F := TypeFun.ofCurried (ITree.Base α)) f b
+
+@[cases_eliminator, elab_as_elim]
+def cases {α ε ρ : Type} {motive : ITree α ε ρ → Sort u}
+    (ret : (r : ρ) → motive (.ret r))
+    (tau : (x : ITree α ε ρ) → motive (.tau x))
+    (vis : (e : ε) → (k : α → ITree α ε ρ) → motive (.vis e k)) :
+    ∀ (x : ITree α ε ρ), motive x :=
+  fun x =>
+    match h : MvQPF.Cofix.dest x with
+    | .ret r =>
+      have h : x = ITree.ret r := by
+        apply_fun MvQPF.Cofix.mk at h
+        simpa [MvQPF.Cofix.mk_dest] using h
+      h ▸ ret r
+    | .tau y =>
+      have h : x = ITree.tau y := by
+        apply_fun MvQPF.Cofix.mk at h
+        simpa [MvQPF.Cofix.mk_dest] using h
+      h ▸ tau y
+    | .vis e k =>
+      have h : x = ITree.vis e k := by
+        apply_fun MvQPF.Cofix.mk at h
+        simpa [MvQPF.Cofix.mk_dest] using h
+      h ▸ vis e k
 
 /-- `ITree.spin` is an infinite sequence of tau-nodes. -/
 def spin : ITree α ε ρ :=
   corec (fun () => .tau ()) ()
 
+inductive EquivUTT.F (R : ITree α ε ρ → ITree α ε ρ → Prop) :
+    ITree α ε ρ → ITree α ε ρ → Prop
+  | ret : EquivUTT.F R (.ret r) (.ret r)
+  | vis :
+    (∀ a, R (k₁ a) (k₂ a))
+    → EquivUTT.F R (.vis e k₁) (.vis e k₂)
+  | tau : R x y → EquivUTT.F R (.tau x) (.tau y)
+  | taul : R x y → EquivUTT.F R (.tau x) y
+  | taur : R x y → EquivUTT.F R x (.tau y)
+
+/-- Equivalence-up-to-tau, i.e., weak bisimiulation.
+
+This is called `eutt` in the Coq development -/
+inductive EquivUTT (x y : ITree α ε ρ) : Prop where
+  | intro (R : ITree α ε ρ → ITree α ε ρ → Prop)
+    (h_fixpoint : ∀ a b, R a b → EquivUTT.F R a b)
+    (h_R : R x y)
+
+namespace EquivUTT
+
+theorem refl (x : ITree α ε ρ) : EquivUTT x x := by
+  apply EquivUTT.intro (R := (· = ·))
+  · rintro a - rfl
+    cases a
+    · constructor
+    · constructor; rfl
+    · constructor; intro; rfl
+  · rfl
+
+theorem symm {x y : ITree α ε ρ} : EquivUTT x y → EquivUTT y x := by
+  rintro ⟨R, isFixpoint, h_R⟩
+  apply EquivUTT.intro (R := flip R)
+  · rintro a b h_fR
+    cases isFixpoint _ _ h_fR
+    <;> constructor
+    <;> assumption
+  · exact h_R
+
+theorem trans {x y z : ITree α ε ρ} : EquivUTT x y → EquivUTT y z → EquivUTT x z := by
+  rintro ⟨R₁, isFixpoint₁, h_R₁⟩ ⟨R₂, isFixpoint₂, h_R₂⟩
+  let R' (a c) := ∃ b, R₁ a b ∧ R₂ b c
+  apply EquivUTT.intro (R := R')
+  · rintro a c ⟨b, h_fR₁, h_fR₂⟩
+    specialize isFixpoint₁ _ _ h_fR₁
+    specialize isFixpoint₂ _ _ h_fR₂
+    clear h_fR₁ h_fR₂
+    -- have r'_of_left (a c) : R' a c
+
+    cases isFixpoint₁
+    case ret r =>
+      generalize ret r = retr
+      -- split at isFixpoint₂
+      -- cases isFixpoint₂
+      · sorry
+    · sorry
+    · sorry
+    · sorry
+    · sorry
+  · exact ⟨y, h_R₁, h_R₂⟩
+
+
+
+end EquivUTT
+
 end ITree