diff --git a/Juvix/Core/Main/Language/Context.lean b/Juvix/Core/Main/Language/Context.lean
index feed2ae..1c0b13f 100644
--- a/Juvix/Core/Main/Language/Context.lean
+++ b/Juvix/Core/Main/Language/Context.lean
@@ -3,7 +3,6 @@ import Juvix.Core.Main.Language.Base
 
 namespace Juvix.Core.Main
 
-
 inductive Context : Type where
   | hole : Context
   | app_left : Context → Expr → Context
diff --git a/Juvix/Core/Main/Semantics/Equiv.lean b/Juvix/Core/Main/Semantics/Equiv.lean
index fdb0456..cf2c770 100644
--- a/Juvix/Core/Main/Semantics/Equiv.lean
+++ b/Juvix/Core/Main/Semantics/Equiv.lean
@@ -35,15 +35,17 @@ def Value.Approx (P : Program) (v v' : Value) : Prop :=
 def Expr.ApproxEvals (P : Program) (env : Env) (e : Expr) (v : Value) : Prop :=
   ∀ n, Expr.ApproxEvals.Indexed P n env e v
 
-notation "⟨" P "⟩ " e " ≲ " e':40 => Value.Approx P e e'
+notation "⟨" P "⟩ " v " ≲ " v':40 => Value.Approx P v v'
 
 notation "⟨" P "⟩ " env " ⊢ " e " ↦≳ " v:40 => Expr.ApproxEvals P env e v
 
 def Expr.Approx (P₁ : Program) (env₁ : Env) (e₁ : Expr) (P₂ : Program) (env₂ : Env) (e₂ : Expr) : Prop :=
   (∀ v, ⟨P₁⟩ env₁ ⊢ e₁ ↦ v → ⟨P₂⟩ env₂ ⊢ e₂ ↦≳ v)
 
+notation "⟨" P "⟩ " env " ⊢ " e " ≲ " "⟨" P' "⟩ " env' " ⊢ " e':40 => Expr.Approx P env e P' env' e'
+
 def Expr.Equiv (P₁ : Program) (env₁ : Env) (e₁ : Expr) (P₂ : Program) (env₂ : Env) (e₂ : Expr) : Prop :=
-  Expr.Approx P₁ env₁ e₁ P₂ env₂ e₂ ∧ Expr.Approx P₂ env₂ e₂ P₁ env₁ e₁
+  ⟨P₁⟩ env₁ ⊢ e₁ ≲ ⟨P₂⟩ env₂ ⊢ e₂ ∧ ⟨P₂⟩ env₂ ⊢ e₂ ≲ ⟨P₁⟩ env₁ ⊢ e₁
 
 notation "⟨" P₁ "⟩ " env₁ " ⊢ " e₁ " ≋ " "⟨" P₂ "⟩ " env₂ " ⊢ " e₂:40 => Expr.Equiv P₁ env₁ e₁ P₂ env₂ e₂
 
@@ -52,7 +54,8 @@ def Program.Equiv (P₁ P₂ : Program) : Prop :=
 
 notation "⟨" P₁ "⟩ " " ≋ " "⟨" P₂ "⟩" => Program.Equiv P₁ P₂
 
-lemma Value.Approx.Indexed.refl {P n v} : Value.Approx.Indexed P n v v := by
+@[refl]
+lemma Value.Approx.Indexed.refl {P n} v : Value.Approx.Indexed P n v v := by
   revert n
   suffices ∀ n, ∀ k ≤ n, Value.Approx.Indexed P k v v by
     intro k
@@ -100,6 +103,7 @@ lemma Value.Approx.Indexed.refl {P n v} : Value.Approx.Indexed P n v v := by
         have : k' ≤ n := by linarith
         aesop
 
+@[trans]
 lemma Value.Approx.Indexed.trans {P n v₁ v₂ v₃} : Value.Approx.Indexed P n v₁ v₂ → Value.Approx.Indexed P n v₂ v₃ → Value.Approx.Indexed P n v₁ v₃ := by
   revert n
   suffices ∀ n, ∀ k ≤ n, Indexed P k v₁ v₂ → Indexed P k v₂ v₃ → Value.Approx.Indexed P k v₁ v₃ by
@@ -164,15 +168,66 @@ lemma Value.Approx.Indexed.trans {P n v₁ v₂ v₃} : Value.Approx.Indexed P n
           have : k' ≤ n := by linarith
           aesop
 
-lemma Value.Approx.refl {P v} : ⟨P⟩ v ≲ v := by
+@[refl]
+lemma Value.Approx.refl {P} v : ⟨P⟩ v ≲ v := by
   intro n
-  exact Value.Approx.Indexed.refl
+  rfl
 
+@[trans]
 lemma Value.Approx.trans {P v₁ v₂ v₃} : ⟨P⟩ v₁ ≲ v₂ → ⟨P⟩ v₂ ≲ v₃ → ⟨P⟩ v₁ ≲ v₃ := by
   intros h₁ h₂
   intro n
   aesop (add unsafe apply Value.Approx.Indexed.trans)
 
+@[simp]
+lemma Value.Approx.unit_left {P v} : ⟨P⟩ v ≲ Value.unit ↔ v = Value.unit := by
+  constructor
+  case mp =>
+    intro h
+    cases h 0
+    rfl
+  case mpr =>
+    intro h
+    subst h
+    rfl
+
+@[simp]
+lemma Value.Approx.unit_right {P v} : ⟨P⟩ Value.unit ≲ v ↔ v = Value.unit := by
+  constructor
+  case mp =>
+    intro h
+    cases h 0
+    rfl
+  case mpr =>
+    intro h
+    subst h
+    rfl
+
+@[simp]
+lemma Value.Approx.const_left {P v c} : ⟨P⟩ v ≲ Value.const c ↔ v = Value.const c := by
+  constructor
+  case mp =>
+    intro h
+    cases h 0
+    rfl
+  case mpr =>
+    intro h
+    subst h
+    rfl
+
+@[simp]
+lemma Value.Approx.const_right {P v c} : ⟨P⟩ Value.const c ≲ v ↔ v = Value.const c := by
+  constructor
+  case mp =>
+    intro h
+    cases h 0
+    rfl
+  case mpr =>
+    intro h
+    subst h
+    rfl
+
+@[aesop unsafe apply]
 lemma Value.Approx.constr_app {P ctr_name args_rev args_rev'} :
   args_rev.length = args_rev'.length →
   (∀ p ∈ List.zip args_rev args_rev', ⟨P⟩ Prod.fst p ≲ Prod.snd p) →
@@ -180,12 +235,14 @@ lemma Value.Approx.constr_app {P ctr_name args_rev args_rev'} :
   intro hlen h n
   aesop
 
+@[aesop unsafe apply]
 lemma Value.Approx.closure {P env₁ body₁ env₂ body₂} :
-  (∀ v v₁, ⟨P⟩ v :: env₁ ⊢ body₁ ↦ v₁ → ⟨P⟩ v :: env₂ ⊢ body₂ ↦≳ v₁) →
+  (∀ v, ⟨P⟩ v :: env₁ ⊢ body₁ ≲ ⟨P⟩ v :: env₂ ⊢ body₂) →
   ⟨P⟩ Value.closure env₁ body₁ ≲ Value.closure env₂ body₂ := by
   intro h n
   aesop
 
+@[aesop safe destruct]
 lemma Value.Approx.constr_app_inv {P ctr_name args_rev args_rev'} :
   ⟨P⟩ Value.constr_app ctr_name args_rev ≲ Value.constr_app ctr_name args_rev' →
   (∀ p ∈ List.zip args_rev args_rev', ⟨P⟩ Prod.fst p ≲ Prod.snd p) ∧
@@ -195,19 +252,153 @@ lemma Value.Approx.constr_app_inv {P ctr_name args_rev args_rev'} :
   case left =>
     intros p hp n
     cases (h (n + 1))
-    case constr_app =>
-      aesop
+    aesop
   case right =>
     cases (h 0)
-    case constr_app =>
-      aesop
+    aesop
 
-lemma Value.Approx.closure_inv {P env₁ body₁ env₂ body₂} :
-  ⟨P⟩ Value.closure env₁ body₁ ≲ Value.closure env₂ body₂ →
-  ∀ v v₁, ⟨P⟩ v :: env₁ ⊢ body₁ ↦ v₁ → ⟨P⟩ v :: env₂ ⊢ body₂ ↦≳ v₁ := by
-  intro h v v₁ h' n
+lemma Value.Approx.constr_app_inv_length {P ctr_name args_rev args_rev'} :
+  ⟨P⟩ Value.constr_app ctr_name args_rev ≲ Value.constr_app ctr_name args_rev' →
+  args_rev.length = args_rev'.length := by
+  intro h
+  exact (Value.Approx.constr_app_inv h).right
+
+lemma Value.Approx.constr_app_inv_args {P ctr_name args_rev args_rev'} :
+  ⟨P⟩ Value.constr_app ctr_name args_rev ≲ Value.constr_app ctr_name args_rev' →
+  ∀ p ∈ List.zip args_rev args_rev', ⟨P⟩ Prod.fst p ≲ Prod.snd p := by
+  intro h
+  exact (Value.Approx.constr_app_inv h).left
+
+@[aesop unsafe 90% destruct]
+lemma Value.Approx.constr_app_inv_left {P ctr_name args_rev' v} :
+  ⟨P⟩ v ≲ Value.constr_app ctr_name args_rev' →
+  ∃ args_rev,
+    v = Value.constr_app ctr_name args_rev ∧
+    args_rev.length = args_rev'.length ∧
+    ∀ p ∈ List.zip args_rev args_rev', ⟨P⟩ Prod.fst p ≲ Prod.snd p := by
+  intro h
+  cases (h 0)
+  aesop
+
+@[aesop unsafe 90% destruct]
+lemma Value.Approx.constr_app_inv_right {P ctr_name args_rev v} :
+  ⟨P⟩ Value.constr_app ctr_name args_rev ≲ v →
+  ∃ args_rev',
+    v = Value.constr_app ctr_name args_rev' ∧
+    args_rev.length = args_rev'.length ∧
+    ∀ p ∈ List.zip args_rev args_rev', ⟨P⟩ Prod.fst p ≲ Prod.snd p := by
+  intro h
+  cases (h 0)
+  aesop
+
+@[aesop safe destruct (immediate := [h])]
+lemma Value.Approx.closure_inv {P env₁ body₁ env₂ body₂}
+  (h : ⟨P⟩ Value.closure env₁ body₁ ≲ Value.closure env₂ body₂) :
+  ∀ v, ⟨P⟩ v :: env₁ ⊢ body₁ ≲ ⟨P⟩ v :: env₂ ⊢ body₂ := by
+  intro v v₁ h' n
   cases (h n.succ)
-  case closure h =>
-    aesop
+  aesop
+
+@[aesop unsafe 90% destruct]
+lemma Value.Approx.closure_inv_left {P env₂ body₂ v} :
+  ⟨P⟩ v ≲ Value.closure env₂ body₂ →
+  ∃ env₁ body₁,
+    v = Value.closure env₁ body₁ ∧
+    (∀ v', ⟨P⟩ v' :: env₁ ⊢ body₁ ≲ ⟨P⟩ v' :: env₂ ⊢ body₂) := by
+  intro h
+  cases (h 0)
+  aesop
+
+@[aesop unsafe 90% destruct]
+lemma Value.Approx.closure_inv_right {P env₁ body₁ v} :
+  ⟨P⟩ Value.closure env₁ body₁ ≲ v →
+  ∃ env₂ body₂,
+    v = Value.closure env₂ body₂ ∧
+    (∀ v', ⟨P⟩ v' :: env₁ ⊢ body₁ ≲ ⟨P⟩ v' :: env₂ ⊢ body₂) := by
+  intro h
+  cases (h 0)
+  aesop
+
+@[aesop safe cases]
+inductive Value.Approx.Inversion (P : Program) : Value -> Value -> Prop where
+  | unit : Value.Approx.Inversion P Value.unit Value.unit
+  | const {c} : Value.Approx.Inversion P (Value.const c) (Value.const c)
+  | constr_app {ctr_name args_rev args_rev'} :
+    args_rev.length = args_rev'.length →
+    (∀ p ∈ List.zip args_rev args_rev', ⟨P⟩ p.1 ≲ p.2) →
+    Value.Approx.Inversion P (Value.constr_app ctr_name args_rev) (Value.constr_app ctr_name args_rev')
+  | closure {env₁ body₁ env₂ body₂} :
+    (∀ v, ⟨P⟩ v :: env₁ ⊢ body₁ ≲ ⟨P⟩ v :: env₂ ⊢ body₂) →
+    Value.Approx.Inversion P (Value.closure env₁ body₁) (Value.closure env₂ body₂)
+
+-- Use `cases (Value.Approx.invert h)` to invert `h : ⟨P⟩ v ≲ v'`.
+@[aesop unsafe destruct]
+lemma Value.Approx.invert {P v v'} :
+  ⟨P⟩ v ≲ v' →
+  Value.Approx.Inversion P v v' := by
+  intro h
+  cases (h 0) <;> constructor <;> aesop
+
+@[aesop unsafe apply]
+lemma Expr.ApproxEvals.equiv {P env e v v'} :
+  ⟨P⟩ env ⊢ e ↦ v' → ⟨P⟩ v' ≲ v → ⟨P⟩ env ⊢ e ↦≳ v := by
+  intro h₁ h₂ n
+  aesop
+
+lemma Expr.ApproxEvals.equiv_inv {P env e v} :
+  ⟨P⟩ env ⊢ e ↦≳ v → ∃ v', ⟨P⟩ env ⊢ e ↦ v' ∧ ⟨P⟩ v' ≲ v := by
+  intro h
+  suffices ∀ n, ∃ v', ⟨P⟩ env ⊢ e ↦ v' ∧ Value.Approx.Indexed P n v' v by
+    obtain ⟨v', h', _⟩ := h 0
+    exists v'
+    constructor
+    · exact h'
+    · intro n
+      obtain ⟨v'', h₁, h₂⟩ := this n
+      have : v' = v'' := by
+        apply Eval.deterministic <;> assumption
+      subst v''
+      simp_all
+  intro n
+  cases (h n)
+  aesop
+
+@[aesop safe cases]
+inductive Expr.ApproxEvals.Inversion (P : Program) (env : Env) (e : Expr) (v : Value) : Prop where
+  | equiv {v'} :
+    ⟨P⟩ env ⊢ e ↦ v' →
+    ⟨P⟩ v' ≲ v →
+    Expr.ApproxEvals.Inversion P env e v
+
+-- Use `cases (Expr.ApproxEvals.invert h)` to invert `h : ⟨P⟩ env ⊢ e ↦≳ v`.
+@[aesop unsafe destruct]
+lemma Expr.ApproxEvals.invert {P env e v} :
+  ⟨P⟩ env ⊢ e ↦≳ v → Expr.ApproxEvals.Inversion P env e v := by
+  intro h
+  cases (Expr.ApproxEvals.equiv_inv h)
+  constructor
+  · aesop (add safe cases And)
+  · aesop
+
+@[aesop unsafe 99% apply]
+lemma Expr.Approx.refl {P env} e : ⟨P⟩ env ⊢ e ≲ ⟨P⟩ env ⊢ e := by
+  intro v
+  aesop
+
+lemma Expr.Approx.rfl {P env e} : ⟨P⟩ env ⊢ e ≲ ⟨P⟩ env ⊢ e :=
+  Expr.Approx.refl e
+
+/-
+lemma Expr.Approx.trans {P₁ env₁ e₁ P₂ env₂ e₂ P₃ env₃ e₃} :
+  ⟨P₁⟩ env₁ ⊢ e₁ ≲ ⟨P₂⟩ env₂ ⊢ e₂ → ⟨P₂⟩ env₂ ⊢ e₂ ≲ ⟨P₃⟩ env₃ ⊢ e₃ → ⟨P₁⟩ env₁ ⊢ e₁ ≲ ⟨P₃⟩ env₃ ⊢ e₃ := by
+  intros h₁ h₂ v hv
+  have h₁' := h₁ v hv
+  cases (Expr.ApproxEvals.invert h₁')
+  case equiv v' hv' ha =>
+    have h₂' := h₂ v' hv'
+    cases (Expr.ApproxEvals.invert h₂')
+    case equiv v'' hv'' ha' =>
+      sorry
+-/
 
 end Juvix.Core.Main