diff --git a/lean/.gitignore b/lean/.gitignore
new file mode 100644
index 00000000..bfb30ec8
--- /dev/null
+++ b/lean/.gitignore
@@ -0,0 +1 @@
+/.lake
diff --git a/lean/Caesar.lean b/lean/Caesar.lean
new file mode 100644
index 00000000..67180077
--- /dev/null
+++ b/lean/Caesar.lean
@@ -0,0 +1,3 @@
+-- This module serves as the root of the `Caesar` library.
+-- Import modules here that should be built as part of the library.
+import «Caesar».Basic
\ No newline at end of file
diff --git a/lean/Caesar/Basic.lean b/lean/Caesar/Basic.lean
new file mode 100644
index 00000000..8f1024f0
--- /dev/null
+++ b/lean/Caesar/Basic.lean
@@ -0,0 +1,526 @@
+import Caesar.Syntax
+import Mathlib.Order.SetNotation
+import Mathlib.Data.Set.Basic
+import Mathlib.Data.Set.Insert
+
+namespace Caesar
+
+@[simp]
+def Expr.Subexprs (e : Expr) : Set Expr := {e} ∪ match e with
+  | .Var _ => {}
+  | .DeBruijn _ => {}
+  | .Quant _ _ ex => ex.Subexprs
+  | [hvl_expr|@x [@_ ↦ @y]] => x.Subexprs ∪ y.Subexprs
+  | .Binary _ l r => l.Subexprs ∪ r.Subexprs
+  | .Unary _ x => x.Subexprs
+  | .Lit _ => {}
+  | .Cast x => x.Subexprs
+  | .Ite c t e => c.Subexprs ∪ t.Subexprs ∪ e.Subexprs
+  | .Call _ args => ⋃ arg ∈ args, arg.Subexprs
+
+@[simp]
+def Expr.splitQuant' (op : QuantOp) (vars : List QuantVar) (e : Expr) : Expr :=
+  match vars with
+  | [] => e
+  | x :: vars => .Quant op [x] (Expr.splitQuant' op vars e)
+
+theorem Expr.splitQuant'_all_one : ∀ e' : (Expr.splitQuant' op vars e).Subexprs,
+  (e'.val ∈ e.Subexprs) ∨
+    match _ : e'.val with
+    | .Quant op vars e => vars.length = 1
+    | _ => true
+:= by
+  induction vars with
+  | nil => simp_all
+  | cons head tail ih => simp_all
+
+@[simp]
+def Expr.splitQuant (e : Expr) : Expr := match _ : e with
+  | .Var x => .Var x
+  | .DeBruijn x => .DeBruijn x
+  | .Quant op vars e => splitQuant' op vars e.splitQuant
+  | [hvl_expr|@x [@i ↦ @y]] =>
+    [hvl_expr|@x.splitQuant [@i ↦ @y.splitQuant]]
+  | .Binary op l r => .Binary op l.splitQuant r.splitQuant
+  | .Unary op x => .Unary op x.splitQuant
+  | .Lit l => .Lit l
+  | .Cast x => .Cast x.splitQuant
+  | .Ite c t e => .Ite c.splitQuant t.splitQuant e.splitQuant
+  | .Call m args => .Call m (args.attach.map (·.val.splitQuant))
+decreasing_by
+  all_goals (try simp [Expr.Cast]; try omega)
+  rename_i x
+  obtain ⟨x, hx⟩ := x
+  simp only
+  have := List.sizeOf_lt_of_mem hx
+  omega
+
+theorem Expr.splitQuant_all_one (e : Expr) : ∀ e' : e.splitQuant.Subexprs,
+  match _ : e'.val with
+  | .Quant _ vars _ => vars.length = 1
+  | _ => true
+:= by
+  simp
+  induction e using splitQuant.induct <;> try simp_all
+  next op vars e ih =>
+    intro e' h
+    split
+    · have := Expr.splitQuant'_all_one (op:=op) (vars:=vars) (e:=e.splitQuant)
+      simp_all
+      replace this := this _ h
+      simp_all
+      rcases this with this | this
+      · have := ih _ this
+        simp_all
+      · assumption
+    · simp_all
+  next => rintro e (he | he) <;> simp_all
+  next op l r ihl ihr => rintro e (he | he) <;> simp_all
+  next => rintro e ((he | he) | he) <;> simp_all
+  next m args ih =>
+    intro e₁ e₂ h₁ h₂
+    exact ih e₂ h₁ e₁ h₂
+
+def Expr.IsDeBruinjN (e : Expr) (n : DeBruijnIndex) : «Bool» := match _ : e with
+  | .Var x => true
+  | .DeBruijn x => x ≤ n
+  | .Quant op vars e =>
+    e.IsDeBruinjN (⟨n.index + vars.length⟩)
+  | [hvl_expr|@x [@i ↦ @y]] =>
+    x.IsDeBruinjN n ∧ y.IsDeBruinjN n
+  | .Binary op l r => l.IsDeBruinjN n ∧ r.IsDeBruinjN n
+  | .Unary op x => x.IsDeBruinjN n
+  | .Lit l => true
+  | .Cast x => x.IsDeBruinjN n
+  | .Ite c t e => c.IsDeBruinjN n ∧ t.IsDeBruinjN n ∧ e.IsDeBruinjN n
+  | .Call m args => args.attach.all (·.val.IsDeBruinjN n)
+termination_by SizeOf.sizeOf e
+decreasing_by
+  all_goals (try simp [Expr.Cast]; try omega)
+  rename_i x
+  obtain ⟨x, hx⟩ := x
+  simp only
+  have := List.sizeOf_lt_of_mem hx
+  omega
+
+def QuantVar.IsDeBruinj (q : QuantVar) : «Bool» := match q with | .DeBrujin => true | _ => false
+
+def Expr.IsDeBruinj (e : Expr) : Prop := ∀ e' ∈ e.Subexprs,
+  match e' with
+  | .Quant _ vars _ => vars.all (·.IsDeBruinj)
+  | _ => true
+
+def QuantVar.name (q : QuantVar) : Ident := match q with
+  | .Shadow s => s
+  | .Fresh v => v.name
+  | .DeBrujin => ⟨"𝒟ℯℬ𝓇𝓊𝒾𝓃𝒿"⟩
+
+@[simp]
+def Expr.deBruinj' (e : Expr) (m : Ident → Option DeBruijnIndex) : Expr := match e with
+  | .Var v => if let some i := m v then .DeBruijn i else .Var v
+  | .Binary op l r =>
+    let l := l.deBruinj' m
+    let r := r.deBruinj' m
+    .Binary op l r
+  | [hvl_expr|@x [@i ↦ @y]] =>
+    let x := x.deBruinj' m
+    let y := y.deBruinj' m
+    [hvl_expr|@x [@i ↦ @y]]
+  | .Quant _ [] exp => exp.deBruinj' m
+  | .Quant op (x :: vars) exp =>
+    let exp := Expr.Quant op vars exp
+    let exp := exp.deBruinj' (fun i ↦ if i = x.name then some 0 else m i |>.map (·.succ))
+    .Quant op [.DeBrujin] exp
+  | .Unary op x => .Unary op (x.deBruinj' m)
+  | .Lit l => .Lit l
+  | .Cast x => .Cast (x.deBruinj' m)
+  | .Ite c t e => .Ite (c.deBruinj' m) (t.deBruinj' m) (e.deBruinj' m)
+  | .Call f args => .Call f $ args.map (·.deBruinj' m)
+  | .DeBruijn i => .DeBruijn i
+
+def Expr.deBruinj (e : Expr) : Expr := e.deBruinj' default
+
+theorem Expr.deBruinj'_IsDeBruinj : (Expr.deBruinj' e m).IsDeBruinj := by
+  induction e, m using Expr.deBruinj'.induct <;> try simp_all [IsDeBruinj]
+  next m op l r ihl ihr => aesop
+  next m i x y ihx ihy => aesop
+  next m op q vars exp exp' ihs => exact And.symm ⟨ihs, rfl⟩
+  next m c t e ihc iht ihe => aesop
+  next m f args ih => exact fun a x a_1 a_2 ↦ ih x a_1 a a_2
+
+theorem Expr.deBruinj_IsDeBruinj : (Expr.deBruinj e).IsDeBruinj := Expr.deBruinj'_IsDeBruinj
+
+/-- info: [hvl_expr|inf dbj. 𝒹₀] -/
+#guard_msgs in
+#eval [hvl_expr|inf x : Int. x].deBruinj
+
+/-- info: [hvl_expr|inf dbj. inf dbj. (𝒹₁ + 𝒹₀)] -/
+#guard_msgs in
+#eval [hvl_expr|inf x : Int. inf y : Int. (x + y)].deBruinj
+
+def Expr.StructuralEquiv (e₁ e₂ : Expr) : «Bool» :=
+  match e₁, e₂ with
+  | .Var v₁, .Var v₂ => v₁ = v₂
+  | .Binary op₁ l₁ r₁, .Binary op₂ l₂ r₂ => op₁ = op₂ ∧ l₁.StructuralEquiv l₂ ∧ r₁.StructuralEquiv r₂
+  | _, _ => false
+
+def Expr.normalize (e : Expr) : Expr := match e with
+  | .Var v => .Var v
+  | .Lit l => .Lit l
+  | [hvl_expr|@x [@i ↦ @y]] => sorry
+
+structure Expr.Equiv (e₁ e₂ : Expr) : Prop where
+  prop : e₁.normalize.StructuralEquiv e₂.normalize
+
+def Expr.is_const : Expr → «Bool»
+| _ => false
+
+structure TyCtx where
+  fresh_counter : Nat
+deriving Inhabited
+
+abbrev TyEnv (α : Type) := StateM TyCtx α
+
+inductive Qq where | Inf | Sup
+
+def QuantVar.getShadow : QuantVar → Option Ident | .Shadow s => some s | _ => none
+
+def Expr.subst (e : Expr) (iter : List (Ident × Expr)) : Expr :=
+  iter.foldl (fun acc (lhs, rhs) ↦ [hvl_expr|@acc [@lhs ↦ @rhs]]) e
+
+/-- info: [hvl_expr|(x + y)[x ↦ z][z ↦ w]] -/
+#guard_msgs in
+#eval [hvl_expr|(x + y)].subst [(⟨"x"⟩, [hvl_expr|z]), (⟨"z"⟩, [hvl_expr|w])]
+
+def Expr.subst_by (e : Expr) (idents : List Ident) (f : Ident → TyEnv Expr) : TyEnv Expr :=
+  return e.subst (← idents.mapM fun ident ↦ return (ident, ← f ident))
+
+instance : ToString Ident where
+  toString i := i.name
+
+def TyCtx.fresh_ident (cx : TyCtx) (ident : Ident) : Ident × TyCtx :=
+  (⟨s!"{ident}𝒻{Nat.toSubscriptString cx.fresh_counter}"⟩, {cx with fresh_counter := cx.fresh_counter + 1})
+
+def TyEnv.fresh_ident (ident : Ident) : TyEnv Ident := do
+  let s ← get
+  let (i, s) := s.fresh_ident ident
+  set s
+  return i
+
+def TyEnv.clone_var (ident : Ident) (kind : VarKind) : TyEnv Ident := do
+  let new_ident := ← TyEnv.fresh_ident ident
+  -- TODO: stuff here
+  return new_ident
+
+def elim_quant (vars : List QuantVar) (opr : Expr) : TyEnv Expr :=
+  let idents := vars.filterMap QuantVar.getShadow
+  opr.subst_by idents fun ident ↦ do
+    let clone_var ← TyEnv.clone_var ident .Quant
+    let fresh_ident := clone_var
+    return .Var fresh_ident
+
+def Expr.qelim : Qq → Expr → TyEnv Expr
+-- Inf
+| .Inf, .Var i => return .Var i
+| .Inf, .Call n args => return .Call n args
+| .Inf, .Ite c lhs rhs => return .Ite c (← lhs.qelim .Inf) (← rhs.qelim .Inf)
+| .Inf, .Binary op a b => match op with
+  | .Add
+  | .And
+  | .Or
+  | .Inf
+  | .Sup =>
+    return .Binary op (← a.qelim .Inf) (← b.qelim .Inf)
+  | .Mul => if a.is_const then return .Binary op a (← b.qelim .Inf) else return .Binary op a b
+  | .Impl | .Compare =>
+      return .Binary op (← a.qelim .Sup) (← b.qelim .Inf)
+  | _ => return .Binary op a b
+| .Inf, .Unary op opr =>
+  if op = .Not then return .Unary op (← opr.qelim .Sup) else return .Unary op opr
+| .Inf, .Cast inner => return .Cast (← inner.qelim .Inf)
+| .Inf, .Quant op vars opr => match op with
+  | .Inf | .Forall =>
+    return ← elim_quant vars (← opr.qelim .Inf)
+  | _ => return .Quant op vars opr
+| .Inf, .Subst a b c => return .Subst a b c
+| .Inf, .Lit a => return .Lit a
+| .Inf, .DeBruijn i => return .DeBruijn i
+-- Sup
+| .Sup, .Var i => return .Var i
+| .Sup, .Call n args => return .Call n args
+| .Sup, .Ite c lhs rhs => return .Ite c (← lhs.qelim .Sup) (← rhs.qelim .Sup)
+| .Sup, .Binary op a b => match op with
+  | .Add
+  | .And
+  | .Or
+  | .Inf
+  | .Sup =>
+    return .Binary op (← a.qelim .Sup) (← b.qelim .Sup)
+  | .Mul => if a.is_const then return .Binary op a (← b.qelim .Sup) else return .Binary op a b
+  | .CoImpl | .CoCompare =>
+      return .Binary op (← a.qelim .Inf) (← b.qelim .Sup)
+  | _ => return .Binary op a b
+| .Sup, .Unary op opr =>
+  if op = .Non then return .Unary op (← opr.qelim .Inf) else return .Unary op opr
+| .Sup, .Cast inner => return .Cast (← inner.qelim .Sup)
+| .Sup, .Quant op vars opr => match op with
+  | .Sup | .Exists =>
+    return ← elim_quant vars (← opr.qelim .Sup)
+  | _ => return .Quant op vars opr
+| .Sup, .Subst a b c => return .Subst a b c
+| .Sup, .Lit a => return .Lit a
+| .Sup, .DeBruijn i => return .DeBruijn i
+
+def TyEnv.eval {α : Type} (f : TyEnv α) : α := (f default).fst
+
+instance : MonadEval TyEnv IO := ⟨(pure ·.eval)⟩
+
+/-- info: [hvl_expr|inf shadow x. x] -/
+#guard_msgs in
+#eval [hvl_expr|inf shadow x. x]
+
+/-- info: [hvl_expr|(x + x)[x ↦ x𝒻₀]] -/
+#guard_msgs in
+#eval [hvl_expr|inf shadow x. (x + x)].qelim .Inf
+
+section Subst
+
+def Expr.free_vars (e : Expr) : List Ident := match e with
+  | .Var x => [x]
+  | _ => []
+
+structure SubstFrame where
+  substs : Std.HashMap Ident Expr
+  free_vars : Std.HashSet Ident
+deriving Inhabited
+
+structure Subst where
+  cur : SubstFrame
+  stack : List SubstFrame
+deriving Inhabited
+def Subst.push_subst (s : Subst) (i : Ident) (x : Expr) : Subst :=
+  let free_vars : Std.HashSet Ident := Std.HashSet.ofList x.free_vars
+  ⟨{s.cur with free_vars := free_vars ∪ s.cur.free_vars, substs := s.cur.substs.insert i x}, s.cur :: s.stack⟩
+def Subst.push_quant (s : Subst) (vars : List QuantVar) : TyEnv (List QuantVar × Subst) := do
+  let fresh ← vars.mapM (TyEnv.fresh_ident ·.name)
+  return Id.run do
+    let mut s := {s with stack := s.cur :: s.stack}
+    let mut new_vars : List QuantVar := []
+    for (var, i) in vars.zipIdx do
+      let ident := var.name
+      s ← {s with cur := {s.cur with substs := s.cur.substs.erase ident}}
+      if s.cur.free_vars.contains ident then
+        let new_ident : Ident := fresh[i]!
+        let new_expr : Expr := .Var new_ident
+        new_vars ← .Shadow new_ident :: new_vars
+        s ← {s with cur := {s.cur with substs := s.cur.substs.insert ident new_expr}}
+      else
+        new_vars ← var :: new_vars
+    return (new_vars, s)
+
+def Subst.push_quant' (cx : TyCtx) (s : Subst) (vars : List QuantVar) : (List QuantVar × Subst × TyCtx) :=
+  vars.foldl (init := ([], {s with stack := s.cur :: s.stack}, cx)) fun (new_vars, s, cx) var ↦
+    let ident := var.name
+    let s := {s with cur :={s.cur with substs := s.cur.substs.erase ident}}
+    if s.cur.free_vars.contains ident then
+      let (new_ident, cx) := cx.fresh_ident ident
+      let new_expr : Expr := .Var new_ident
+      (.Shadow new_ident :: new_vars, {s with cur := {s.cur with substs := s.cur.substs.insert ident new_expr}}, cx)
+    else
+      (var :: new_vars, s, cx)
+
+def Subst.lookup_var (s : Subst) (ident : Ident) : Option Expr :=
+  s.cur.substs.get? ident
+
+def Expr.perform_subst (e : Expr) (subst : Caesar.Subst) : TyEnv Expr := match e with
+  | .Var x => return if let some e' := subst.lookup_var x then e' else e
+  | .DeBruijn i => return .DeBruijn i
+  | .Quant op vars e => do
+    let (vars, subst) ← subst.push_quant vars
+    return .Quant op vars (← e.perform_subst subst)
+  | [hvl_expr|@x [@i ↦ @y]] => do
+    let y' := ← y.perform_subst subst
+    x.perform_subst (subst.push_subst i y')
+  | .Binary op l r => return .Binary op (← l.perform_subst subst) (← r.perform_subst subst)
+  | .Unary op x => return .Unary op (← x.perform_subst subst)
+  | .Lit l => return .Lit l
+  | .Cast x => return .Cast (← x.perform_subst subst)
+  | .Ite c t e => return .Ite (← c.perform_subst subst) (← t.perform_subst subst) (← e.perform_subst subst)
+  | .Call m args => return .Call m (← args.mapM (·.perform_subst subst))
+
+def Expr.perform_subst' (e : Expr) (cx : TyCtx) (subst : Caesar.Subst) : Expr × TyCtx := match e with
+  | .Var x => (if let some e' := subst.lookup_var x then e' else e, cx)
+  | .DeBruijn i => (.DeBruijn i, cx)
+  | .Quant op vars e =>
+    let (vars, subst, cx) := subst.push_quant' cx vars
+    let (e, cx) := e.perform_subst' cx subst
+    (.Quant op vars e, cx)
+  | [hvl_expr|@x [@i ↦ @y]] =>
+    let (y', cx) := y.perform_subst' cx subst
+    x.perform_subst' cx (subst.push_subst i y')
+  | .Binary op l r =>
+    let (l, cx) := l.perform_subst' cx subst
+    let (r, cx) := r.perform_subst' cx subst
+    (.Binary op l r, cx)
+  | .Unary op x =>
+    let (x, cx) := x.perform_subst' cx subst
+    (.Unary op x, cx)
+  | .Lit l => (.Lit l, cx)
+  | .Cast x => let (x, cx) := x.perform_subst' cx subst; (.Cast x, cx)
+  | .Ite c t e =>
+    let (c, cx) := c.perform_subst' cx subst
+    let (t, cx) := t.perform_subst' cx subst
+    let (e, cx) := e.perform_subst' cx subst
+    (.Ite c t e, cx)
+  | .Call m args =>
+    let (args, cx) := args.foldl (init := ([], cx)) fun (args, cx) arg ↦
+      let (arg, cx) := arg.perform_subst' cx subst
+      (arg :: args, cx)
+    (.Call m args, cx)
+
+def Expr.apply_subst : Expr → TyEnv Expr := (·.perform_subst default)
+def Expr.apply_subst' (cx : TyCtx) : Expr → Expr × TyCtx := (·.perform_subst' cx default)
+
+/-- info: [hvl_expr|y] -/
+#guard_msgs in
+#eval [hvl_expr|x[x ↦ y]].apply_subst' default |>.1
+/-- info: [hvl_expr|(inf shadow y. y + a + inf shadow y. y)] -/
+#guard_msgs in
+#eval [hvl_expr|(x + a + x)[x ↦ inf shadow y. y]].apply_subst' default |>.1
+
+/-- info: [hvl_expr|(y + inf x: Int. (x + y))] -/
+#guard_msgs in
+#eval [hvl_expr|(x + inf x: Int. (x + y))[x ↦ y]].apply_subst' default |>.1
+
+/-- info: [hvl_expr|(inf shadow x𝒻₀. (x𝒻₀ + x))] -/
+#guard_msgs in
+#eval [hvl_expr|(inf x: Int. (x + y))[y ↦ x]].apply_subst' default |>.1
+
+end Subst
+
+section Semantics
+
+inductive Value where
+  | Bool : «Bool» → Value
+  | Int : «Int» → Value
+  | Missing
+deriving Inhabited
+
+def Value.Bool? : Value → Option _root_.Bool
+| .Bool b => some b
+| _ => none
+def Value.Int? : Value → Option _root_.Int
+| .Int b => some b
+| _ => none
+
+structure Memory where
+  values : Std.HashMap Ident Value
+
+instance : Coe _root_.Bool Value where
+  coe := .Bool
+
+def Memory.subst (σ : Memory) (ident : Ident) (value : Value) : Memory :=
+  ⟨σ.values.insert ident value⟩
+
+def Expr.eval (e : Expr) (σ : Memory) : Option Value := match e with
+  | .Var x => σ.values.get? x
+  | [hvl_expr|!@e] => return !(← (← e.eval σ).Bool?)
+  | [hvl_expr|(@e)] => e.eval σ
+  -- | [hvl_expr|@l + @r] => return .Int $ (← (← l.eval σ).Int?) + (← (← r.eval σ).Int?)
+  | [hvl_expr|@l + @r] => match _ : l.eval σ, r.eval σ with
+    | some (.Int l), some (.Int r) => some (.Int (l + r))
+    | _, _ => none
+  | [hvl_expr|@x [@i ↦ @y]] => return ← x.eval (σ.subst i (← y.eval σ))
+  | _ => none
+
+/-- info: Caesar.Value.Int 3 -/
+#guard_msgs in
+#eval [hvl_expr|x + y].eval ⟨Std.HashMap.ofList [(⟨"x"⟩, .Int 1), (⟨"y"⟩, .Int 2)]⟩ |>.getD .Missing
+
+/-- info: Caesar.Value.Int 4 -/
+#guard_msgs in
+#eval [hvl_expr|(x + y)[x ↦ y]].eval ⟨Std.HashMap.ofList [(⟨"x"⟩, .Int 1), (⟨"y"⟩, .Int 2)]⟩ |>.getD .Missing
+
+theorem Expr.perform_subst_var : (Expr.Var x).perform_subst s = do match s.lookup_var x with | some x' => return x' | none => return Expr.Var x := by
+  simp [TyEnv.eval, default, perform_subst, pure, StateT.pure]
+  aesop
+
+@[simp]
+theorem asdasd (s : Subst) : (s.push_subst a x).lookup_var b = if a = b then some x else s.lookup_var b := by
+  simp [Subst.push_subst, Subst.lookup_var]
+  split_ifs
+  · simp_all
+  · simp_all [Std.HashMap.getElem?_insert]
+
+@[simp] theorem asjhdasjhd : Subst.lookup_var default s = none := by simp [Subst.lookup_var, default]
+
+def Subst.vars (s : Subst) : List Ident := s.cur.substs.keys
+
+def Memory.subst' (σ : Memory) (s : Subst) : Memory :=
+  let s' : Std.HashMap Ident Value := s.cur.substs.map (fun _ b ↦ b.eval σ |>.getD .Missing)
+  ⟨σ.values ∪ s'⟩
+
+protected def Std.HashMap.getElem_union {α : Type} {β : Type} [BEq α] [Hashable α] (m₁ m₂ : Std.HashMap α β) (j : α) : (m₁ ∪ m₂)[j]? = m₁[j]?.or m₂[j]? := by
+  ext x
+  simp [Std.HashMap.instUnion]
+  simp [Std.HashMap.union]
+  sorry
+
+@[simp]
+theorem ashdjashdj (σ : Memory) : (σ.subst' s).values[j]? = if let some e := s.lookup_var j then e.eval σ else σ.values.get? j := by
+  ext v
+  simp [Memory.subst']
+  simp [Std.HashMap.getElem_union]
+  split
+  · simp_all
+  · simp_all
+
+theorem askjdas (e : Expr) : (e.perform_subst' cx s).1.eval σ = e.eval (σ.subst' s) := by
+  ext v
+  induction e, σ using Expr.eval.induct generalizing v cx s
+  next σ j =>
+    simp [Expr.apply_subst', Expr.perform_subst', Expr.eval]
+    split <;> simp_all [Expr.eval]
+  next σ x ih =>
+    -- simp_all [Expr.eval]
+    simp_all [Expr.perform_subst']
+    simp [Expr.eval, Expr.perform_subst']
+
+    simp_all [Expr.apply_subst, Expr.perform_subst, pure, StateT.pure, TyEnv.eval, Expr.eval, Value.Bool?]
+    -- aesop
+    sorry
+  next σ e ih => simp_all [Expr.apply_subst', Expr.perform_subst', Expr.eval]
+  next σ l r lv rv hl hr ihl ihr =>
+    simp_all [Expr.apply_subst', Expr.perform_subst', Expr.eval, Value.Int?]
+    split <;> split <;> simp_all <;> subst_eqs
+    · congr!
+      sorry
+    ·
+      rintro ⟨_⟩
+      rename_i h _
+      contrapose! h
+      simp_all
+      exists lv
+      have := ihl (.Int lv)
+      simp_all
+
+
+      have := h lv rv
+      simp at this
+
+      have h₁ := ihr (.Int rv)
+      have h₂ := ihl (.Int lv)
+      simp at h₁ h₂
+      simp_all
+      sorry
+  next =>
+    simp_all
+    sorry
+  next =>
+    simp_all [Expr.apply_subst', Expr.perform_subst', Expr.eval, Value.Int?]
+
+    sorry
+
+end Semantics
+
+end Caesar
diff --git a/lean/Caesar/Expr.lean b/lean/Caesar/Expr.lean
new file mode 100644
index 00000000..20e817cc
--- /dev/null
+++ b/lean/Caesar/Expr.lean
@@ -0,0 +1,190 @@
+import Batteries.Data.Rat.Basic
+import Lean.ToExpr
+import Mathlib.Data.Rat.Lemmas
+
+namespace Caesar
+
+structure Ident where
+  name : String
+deriving Lean.ToExpr, DecidableEq, Hashable, Inhabited
+
+inductive BinOp where
+  /- The `+` operator (addition). -/
+  | Add
+  /- The `-` operator (subtraction). -/
+  | Sub
+  /- The `*` operator (multiplication). -/
+  | Mul
+  /- The `/` operator (divison). -/
+  | Div
+  /- The `%` operator (modulo). -/
+  | Mod
+  /- The `&&` operator (logical and). -/
+  | And
+  /- The `||` operator (logical or). -/
+  | Or
+  /- The `==` operator (equality). -/
+  | Eq
+  /- The `<` operator (less than). -/
+  | Lt
+  /- The `<=` operator (less than or equal to). -/
+  | Le
+  /- The `!=` operator (not equal to). -/
+  | Ne
+  /- The `>=` operator (greater than or equal to). -/
+  | Ge
+  /- The `>` operator (greater than). -/
+  | Gt
+  /- The `⊓` operator (infimum). -/
+  | Inf
+  /- The `⊔` operator (supremum). -/
+  | Sup
+  /- The `→` operator (implication). -/
+  | Impl
+  /- The `←` operator (co-implication). -/
+  | CoImpl
+  /- The `↘` operator (hard implication/compare). -/
+  | Compare
+  /- The `↖` operator (hard co-implication/co-compare). -/
+  | CoCompare
+deriving Lean.ToExpr, DecidableEq
+
+inductive UnOp where
+  /- The `!` operator (negation). -/
+  | Not
+  /- The `~` operator (dual of negation), -/
+  | Non
+  /- Boolean embedding (maps true to top in the lattice). -/
+  | Embed
+  /- Iverson bracket (maps true to 1). -/
+  | Iverson
+  /- Parentheses (just to print ASTs faithfully). -/
+  | Parens
+deriving Lean.ToExpr, DecidableEq
+
+inductive QuantOp where
+  /- The infimum of a set. -/
+  | Inf
+  /- The supremum of a set. -/
+  | Sup
+  /- Boolean forall (equivalent to `Inf` on the lattice of booleans). -/
+  | Forall
+  /- Boolean exists (equivalent to `Sup` on the lattice of booleans). -/
+  | Exists
+deriving Lean.ToExpr, DecidableEq
+
+inductive Ty where
+  /- The primitive boolean type `Bool`. -/
+  | Bool
+  /- A signed integer type. -/
+  | Int
+  /- A unsigned integer type. -/
+  | UInt
+  /- Real numbers. -/
+  | Real
+  /- Unsigned real numbers -/
+  | UReal
+  /- Unsigned real numbers with infinity. -/
+  | EUReal
+deriving Lean.ToExpr, DecidableEq
+
+inductive VarKind where
+  /- Input parameters (cannot be modified). -/
+  | Input
+  /- Output parameters (cannot be accessed in the pre). -/
+  | Output
+  /- Mutable variables. -/
+  | Mut
+  /- Variables bound by a quantifier. -/
+  | Quant
+  /- Variables from a substitution (cannot be modified). -/
+  | Subst
+  /- Variables for slicing (cannot be modified). -/
+  | Slice
+deriving Lean.ToExpr, DecidableEq
+
+structure VarDecl where
+  name : Ident
+  ty : Ty
+  kind : VarKind
+deriving Lean.ToExpr, DecidableEq
+
+structure DeBruijnIndex where
+  index : Nat
+deriving Lean.ToExpr, DecidableEq
+
+inductive QuantVar where
+  | Shadow : Ident → QuantVar
+  | Fresh : VarDecl → QuantVar
+  | DeBrujin : QuantVar
+deriving Lean.ToExpr, DecidableEq
+
+structure Trigger where
+  -- TODO: these makes expr cyclic which can prevent induction. add later
+  terms : List Unit
+deriving Lean.ToExpr, DecidableEq
+
+-- structure QuantAnn where
+--   triggers : List Trigger
+-- deriving Lean.ToExpr, DecidableEq
+
+structure Symbol where
+  name : String
+deriving Lean.ToExpr, DecidableEq
+
+open Lean in
+instance : Lean.ToExpr Rat where
+  toExpr r :=
+    if r.den == 1 then toExpr r.num else  mkApp2 (.const ``Div.div []) (toExpr r.num) (toExpr r.den)
+  toTypeExpr := .const ``Rat []
+
+inductive Lit where
+  /- A string literal (`"something"`). -/
+  | Str : String → Lit
+  /- An unsigned integer literal (`123`). -/
+  -- TODO: this should have been u128
+  | UInt : UInt64 → Lit
+  /- A number literal represented by a fraction. -/
+  | Frac : Rat → Lit
+  /- Infinity, -/
+  | Infinity : Lit
+  /- A boolean literal. -/
+  | Bool : Bool → Lit
+deriving Lean.ToExpr, DecidableEq
+
+inductive Expr where
+  /- A variable. -/
+  | Var : Ident → Expr
+  /- A call to a procedure or function. -/
+  | Call : Ident → List Expr → Expr
+  /- Boolean if-then-else -/
+  | Ite : Expr → Expr → Expr → Expr
+  /- Use of a binary operator. -/
+  | Binary : BinOp → Expr → Expr → Expr
+  /- Use of an unary operator. -/
+  | Unary : UnOp → Expr → Expr
+  /- Type casting. -/
+  | Cast : Expr → Expr
+  /- A quantifier over some variables. -/
+  | Quant : QuantOp → List QuantVar → Expr → Expr
+  /- A substitution. -/
+  | Subst : Ident → Expr → Expr → Expr
+  /- A value literal. -/
+  | Lit : Lit → Expr
+  /- A de Bruijn index. -/
+  | DeBruijn : DeBruijnIndex → Expr
+deriving Lean.ToExpr, Inhabited
+
+instance (n : Nat) : OfNat DeBruijnIndex n := ⟨⟨n⟩⟩
+
+def DeBruijnIndex.succ (i : DeBruijnIndex) : DeBruijnIndex := ⟨i.index + 1⟩
+
+instance : LinearOrder DeBruijnIndex where
+  le a b := a.index ≤ b.index
+  le_refl := by simp
+  le_trans := fun _ _ _ ↦ Nat.le_trans
+  le_antisymm := fun ⟨_⟩ ⟨_⟩ ↦ by simp; exact Nat.le_antisymm
+  le_total := fun ⟨_⟩ ⟨_⟩ ↦ by simp; apply Nat.le_total
+  decidableLE a b := if h : a.index ≤ b.index then .isTrue h else .isFalse h
+
+end Caesar
diff --git a/lean/Caesar/Syntax.lean b/lean/Caesar/Syntax.lean
new file mode 100644
index 00000000..73eaf775
--- /dev/null
+++ b/lean/Caesar/Syntax.lean
@@ -0,0 +1,306 @@
+import Caesar.Expr
+
+namespace Caesar
+
+open Lean PrettyPrinter
+
+declare_syntax_cat hvl_ident
+syntax "[hvl_ident|" hvl_ident "]" : term
+declare_syntax_cat hvl_expr
+syntax "[hvl_expr|" hvl_expr "]" : term
+declare_syntax_cat hvl_ty
+syntax "[hvl_ty|" hvl_ty "]" : term
+declare_syntax_cat hvl_quant_op
+syntax "[hvl_quant_op|" hvl_quant_op "]" : term
+declare_syntax_cat hvl_quant_var
+syntax "[hvl_quant_var|" hvl_quant_var "]" : term
+declare_syntax_cat hvl_quant_ann
+syntax "[hvl_quant_ann|" hvl_quant_ann "]" : term
+declare_syntax_cat hvl_var_decl
+syntax "[hvl_var_decl|" hvl_var_decl "]" : term
+
+syntax "inf" : hvl_quant_op
+syntax "sup" : hvl_quant_op
+syntax "exists" : hvl_quant_op
+syntax "forall" : hvl_quant_op
+
+syntax ident : hvl_ident
+syntax "@" term:max : hvl_ident
+
+syntax "Int" : hvl_ty
+syntax "Bool" : hvl_ty
+syntax "UInt" : hvl_ty
+syntax "Real" : hvl_ty
+syntax "UReal" : hvl_ty
+syntax "EUReal" : hvl_ty
+
+syntax hvl_ident ": " hvl_ty : hvl_var_decl
+
+syntax hvl_var_decl : hvl_quant_var
+syntax "shadow " hvl_ident : hvl_quant_var
+syntax "dbj" : hvl_quant_var
+
+syntax hvl_ident : hvl_expr
+syntax hvl_expr "[" hvl_ident " ↦ " hvl_expr "]" : hvl_expr
+syntax hvl_quant_op hvl_quant_var+ ". " hvl_expr : hvl_expr
+syntax hvl_quant_op hvl_quant_var+ ". " hvl_expr : hvl_expr
+
+syntax "@" term:max : hvl_expr
+
+section Operators
+
+syntax:50 hvl_expr:50 " + " hvl_expr:50 : hvl_expr
+syntax:50 hvl_expr:50 " - " hvl_expr:50 : hvl_expr
+syntax:50 hvl_expr:50 " * " hvl_expr:50 : hvl_expr
+syntax:50 hvl_expr:50 " / " hvl_expr:50 : hvl_expr
+syntax:50 hvl_expr:50 " % " hvl_expr:50 : hvl_expr
+syntax:50 hvl_expr:50 " && " hvl_expr:50 : hvl_expr
+syntax:50 hvl_expr:50 " || " hvl_expr:50 : hvl_expr
+syntax:50 hvl_expr:50 " == " hvl_expr:50 : hvl_expr
+syntax:50 hvl_expr:50 " < " hvl_expr:50 : hvl_expr
+syntax:50 hvl_expr:50 " <= " hvl_expr:50 : hvl_expr
+syntax:50 hvl_expr:50 " != " hvl_expr:50 : hvl_expr
+syntax:50 hvl_expr:50 " >= " hvl_expr:50 : hvl_expr
+syntax:50 hvl_expr:50 " > " hvl_expr:50 : hvl_expr
+syntax:50 hvl_expr:50 " ⊓ " hvl_expr:50 : hvl_expr
+syntax:50 hvl_expr:50 " ⊔ " hvl_expr:50 : hvl_expr
+syntax:50 hvl_expr:50 " → " hvl_expr:50 : hvl_expr
+syntax:50 hvl_expr:50 " ← " hvl_expr:50 : hvl_expr
+syntax:50 hvl_expr:50 " ↘ " hvl_expr:50 : hvl_expr
+syntax:50 hvl_expr:50 " ↖ " hvl_expr:50 : hvl_expr
+
+syntax "!" hvl_expr : hvl_expr
+syntax "~" hvl_expr : hvl_expr
+syntax "[" hvl_expr "]" : hvl_expr
+syntax "(" hvl_expr ")" : hvl_expr
+
+-- TODO:
+-- /- Boolean embedding (maps true to top in the lattice). -/
+-- | Embed
+
+macro_rules
+-- binary
+| `([hvl_expr|$l + $r]) => `(Expr.Binary BinOp.Add [hvl_expr|$l] [hvl_expr|$r])
+| `([hvl_expr|$l - $r]) => `(Expr.Binary BinOp.Sub [hvl_expr|$l] [hvl_expr|$r])
+| `([hvl_expr|$l * $r]) => `(Expr.Binary BinOp.Mul [hvl_expr|$l] [hvl_expr|$r])
+| `([hvl_expr|$l / $r]) => `(Expr.Binary BinOp.Div [hvl_expr|$l] [hvl_expr|$r])
+| `([hvl_expr|$l % $r]) => `(Expr.Binary BinOp.Mod [hvl_expr|$l] [hvl_expr|$r])
+| `([hvl_expr|$l && $r]) => `(Expr.Binary BinOp.And [hvl_expr|$l] [hvl_expr|$r])
+| `([hvl_expr|$l || $r]) => `(Expr.Binary BinOp.Or [hvl_expr|$l] [hvl_expr|$r])
+| `([hvl_expr|$l == $r]) => `(Expr.Binary BinOp.Eq [hvl_expr|$l] [hvl_expr|$r])
+| `([hvl_expr|$l < $r]) => `(Expr.Binary BinOp.Lt [hvl_expr|$l] [hvl_expr|$r])
+| `([hvl_expr|$l <= $r]) => `(Expr.Binary BinOp.Le [hvl_expr|$l] [hvl_expr|$r])
+| `([hvl_expr|$l != $r]) => `(Expr.Binary BinOp.Ne [hvl_expr|$l] [hvl_expr|$r])
+| `([hvl_expr|$l >= $r]) => `(Expr.Binary BinOp.Ge [hvl_expr|$l] [hvl_expr|$r])
+| `([hvl_expr|$l > $r]) => `(Expr.Binary BinOp.Gt [hvl_expr|$l] [hvl_expr|$r])
+| `([hvl_expr|$l ⊓ $r]) => `(Expr.Binary BinOp.Inf [hvl_expr|$l] [hvl_expr|$r])
+| `([hvl_expr|$l ⊔ $r]) => `(Expr.Binary BinOp.Sup [hvl_expr|$l] [hvl_expr|$r])
+| `([hvl_expr|$l → $r]) => `(Expr.Binary BinOp.Impl [hvl_expr|$l] [hvl_expr|$r])
+| `([hvl_expr|$l ← $r]) => `(Expr.Binary BinOp.CoImpl [hvl_expr|$l] [hvl_expr|$r])
+| `([hvl_expr|$l ↘ $r]) => `(Expr.Binary BinOp.Compare [hvl_expr|$l] [hvl_expr|$r])
+| `([hvl_expr|$l ↖ $r]) => `(Expr.Binary BinOp.CoCompare [hvl_expr|$l] [hvl_expr|$r])
+-- unary
+| `([hvl_expr|! $x:hvl_expr]) => `(Expr.Unary .Not [hvl_expr|$x])
+| `([hvl_expr|~ $x:hvl_expr]) => `(Expr.Unary .Non [hvl_expr|$x])
+| `([hvl_expr|[$x:hvl_expr]]) => `(Expr.Unary .Iverson [hvl_expr|$x])
+| `([hvl_expr|($x:hvl_expr)]) => `(Expr.Unary .Parens [hvl_expr|$x])
+
+end Operators
+
+macro_rules
+| `([hvl_ident| $n:ident ]) => `(term|({name:=$(quote n.getId.toString)} : Ident))
+| `([hvl_ident| @$n:term ]) => `($n)
+
+open Lean in
+macro_rules
+-- types
+| `([hvl_ty|Int]) => `(Ty.Int)
+| `([hvl_ty|Bool]) => `(Ty.Bool)
+-- var decl
+| `([hvl_var_decl|$x:hvl_ident : $ty]) => `(VarDecl.mk [hvl_ident|$x] [hvl_ty|$ty])
+-- quant op
+| `([hvl_quant_op|inf]) => `(QuantOp.Inf)
+| `([hvl_quant_op|sup]) => `(Caesar.QuantOp.Sup)
+| `([hvl_quant_op|exists]) => `(Caesar.QuantOp.Exists)
+| `([hvl_quant_op|forall]) => `(Caesar.QuantOp.Forall)
+-- quant var
+| `([hvl_quant_var|$x:hvl_var_decl]) => `(QuantVar.Fresh ([hvl_var_decl|$x] .Quant))
+| `([hvl_quant_var|shadow $x:hvl_ident]) => `(QuantVar.Shadow [hvl_ident|$x])
+| `([hvl_quant_var|dbj]) => `(QuantVar.DeBrujin)
+-- expr
+| `([hvl_expr|$i:hvl_ident]) => `(Caesar.Expr.Var [hvl_ident|$i])
+| `([hvl_expr|$x[$a ↦ $b]]) => `(Caesar.Expr.Subst [hvl_ident|$a] [hvl_expr|$x] [hvl_expr|$b])
+| `([hvl_expr|inf $ann*. $e]) => `(Caesar.Expr.Quant .Inf [$[[hvl_quant_var|$ann]],*] [hvl_expr|$e])
+| `([hvl_expr|sup $ann*. $e]) => `(Caesar.Expr.Quant .Sup [$[[hvl_quant_var|$ann]],*] [hvl_expr|$e])
+| `([hvl_expr|exists $ann*. $e]) => `(Caesar.Expr.Quant .Exists [$[[hvl_quant_var|$ann]],*] [hvl_expr|$e])
+| `([hvl_expr|forall $ann*. $e]) => `(Caesar.Expr.Quant .Forall [$[[hvl_quant_var|$ann]],*] [hvl_expr|$e])
+| `([hvl_expr|@ $e]) => `($e)
+
+/-- info: QuantVar.Fresh { name := { name := "x" }, ty := Ty.Int, kind := VarKind.Quant } -/
+#guard_msgs in
+#eval [hvl_quant_var|x : Int]
+
+/--
+info: Expr.Quant QuantOp.Inf [QuantVar.Fresh { name := { name := "x" }, ty := Ty.Int, kind := VarKind.Quant }]
+  (Expr.Var { name := "x" })
+-/
+#guard_msgs in
+#eval [hvl_expr|inf x : Int. x]
+
+/-- info: Expr.Quant QuantOp.Inf [QuantVar.DeBrujin] (Expr.Var { name := "x" }) -/
+#guard_msgs in
+#eval [hvl_expr|inf dbj . x]
+
+@[app_unexpander Caesar.Expr.Var]
+def Expr.unexpandVar : Unexpander
+| `($_lit $s) =>
+  match s with
+    | `({name:=$y:str}) =>
+      let name := mkIdent $ Name.mkSimple y.getString
+      `([hvl_expr|$name:ident])
+    | _ =>
+      `([hvl_expr|@$s])
+| _ => throw ()
+
+/-- info: [hvl_expr|x] -/
+#guard_msgs in
+#eval [hvl_expr|x]
+
+/-- info: fun x ↦ [hvl_expr|@x] : Ident → Expr -/
+#guard_msgs in
+#check fun (x : Ident) ↦ Expr.Var x
+
+@[app_unexpander Caesar.Expr.Subst]
+def Expr.unexpandSubst : Unexpander
+| `($_lit {name:=$a:str} [hvl_expr|$x] [hvl_expr|$b]) =>
+  let a := mkIdent $ Name.mkSimple a.getString
+  `([hvl_expr|$x[$a:ident ↦ $b]])
+| _ => throw ()
+
+/-- info: [hvl_expr|a[b ↦ c]] -/
+#guard_msgs in
+#eval [hvl_expr|a[b ↦ c]]
+
+open Lean in
+@[app_unexpander Caesar.Expr.Quant]
+def Expr.unexpandQuant : Unexpander
+| `($_lit $op $vars* $e) => do
+  let e ← match e with | `([hvl_expr|$e]) => `(hvl_expr|$e) | _ => `(hvl_expr|@$e)
+  match vars[0]! with
+  -- | `([QuantVar.Fresh {name:=$x:str}]) => mkIdent $ Name.mkSimple x.getString
+  | `([QuantVar.Fresh {name:={name:=$x:str},ty:=$y,kind:=$z}]) =>
+    let ty : UnexpandM (TSyntax `hvl_ty) := match y with
+      | `(Ty.Int) => `(hvl_ty|Int)
+      | `(Ty.Bool) => `(hvl_ty|Bool)
+      | `(Ty.UInt) => `(hvl_ty|UInt)
+      | `(Ty.Real) => `(hvl_ty|Real)
+      | `(Ty.UReal) => `(hvl_ty|UReal)
+      | `(Ty.EUReal) => `(hvl_ty|EUReal)
+      | _ => `(hvl_ty|Int)
+    let name := mkIdent $ Name.mkSimple x.getString
+    let ty ← ty
+    match op with
+    | `(QuantOp.Inf) => `([hvl_expr|inf $name:ident : $ty. $e])
+    | `(QuantOp.Sup) => `([hvl_expr|sup $name:ident : $ty. $e])
+    | `(QuantOp.Exists) => `([hvl_expr|exists $name:ident : $ty. $e])
+    | `(QuantOp.Forall) => `([hvl_expr|forall $name:ident : $ty. $e])
+    | _ => `(hi)
+  | `([QuantVar.Shadow {name:=$x:str}]) =>
+    let name := mkIdent $ Name.mkSimple x.getString
+    match op with
+    | `(QuantOp.Inf) => `([hvl_expr|inf shadow $name:ident. $e])
+    | `(QuantOp.Sup) => `([hvl_expr|sup shadow $name:ident. $e])
+    | `(QuantOp.Exists) => `([hvl_expr|exists shadow $name:ident. $e])
+    | `(QuantOp.Forall) => `([hvl_expr|forall shadow $name:ident. $e])
+    | _ => `(hi)
+  | `([QuantVar.DeBrujin]) =>
+    -- let name := mkIdent $ Name.mkSimple x.getString
+    match op with
+    | `(QuantOp.Inf) => `([hvl_expr|inf dbj. $e])
+    | `(QuantOp.Sup) => `([hvl_expr|sup dbj. $e])
+    | `(QuantOp.Exists) => `([hvl_expr|exists dbj. $e])
+    | `(QuantOp.Forall) => `([hvl_expr|forall dbj. $e])
+    | _ => `(hi)
+  | _ => throw ()
+| _ => throw ()
+
+/-- info: [hvl_expr|inf shadow x. x] -/
+#guard_msgs in
+#eval [hvl_expr|inf shadow x. x]
+
+/-- info: [hvl_expr|inf a: Bool. x] -/
+#guard_msgs in
+#eval [hvl_expr|inf a: Bool. x]
+
+/-- info: [hvl_expr|inf dbj. x] -/
+#guard_msgs in
+#eval [hvl_expr|inf dbj . x]
+
+/-- info: [hvl_expr|a[b ↦ c]] -/
+#guard_msgs in
+#eval [hvl_expr|a[b ↦ c]]
+
+open Lean in
+@[app_unexpander Caesar.Expr.Binary]
+def Expr.unexpandBinary : Unexpander
+| `($_bin $op $l $r) => do
+  let l ← match l with | `([hvl_expr|$l]) => `(hvl_expr|$l) | _ => `(hvl_expr|@$l)
+  let r ← match r with | `([hvl_expr|$r]) => `(hvl_expr|$r) | _ => `(hvl_expr|@$r)
+  match op with
+    | `(BinOp.Add) => `([hvl_expr|$l + $r])
+    | `(BinOp.Sub) => `([hvl_expr|$l - $r])
+    | `(BinOp.Mul) => `([hvl_expr|$l * $r])
+    | `(BinOp.Div) => `([hvl_expr|$l / $r])
+    | `(BinOp.Mod) => `([hvl_expr|$l % $r])
+    | `(BinOp.And) => `([hvl_expr|$l && $r])
+    | `(BinOp.Or) => `([hvl_expr|$l || $r])
+    | `(BinOp.Eq) => `([hvl_expr|$l == $r])
+    | `(BinOp.Lt) => `([hvl_expr|$l < $r])
+    | `(BinOp.Le) => `([hvl_expr|$l <= $r])
+    | `(BinOp.Ne) => `([hvl_expr|$l != $r])
+    | `(BinOp.Ge) => `([hvl_expr|$l >= $r])
+    | `(BinOp.Gt) => `([hvl_expr|$l > $r])
+    | `(BinOp.Inf) => `([hvl_expr|$l ⊓ $r])
+    | `(BinOp.Sup) => `([hvl_expr|$l ⊔ $r])
+    | `(BinOp.Impl) => `([hvl_expr|$l → $r])
+    | `(BinOp.CoImpl) => `([hvl_expr|$l ← $r])
+    | `(BinOp.Compare) => `([hvl_expr|$l ↘ $r])
+    | `(BinOp.CoCompare) => `([hvl_expr|$l ↖ $r])
+    | _ => throw ()
+| _ => throw ()
+
+open Lean in
+@[app_unexpander Caesar.Expr.Unary]
+def Expr.unexpandUnary : Unexpander
+| `($_un $op $x) => do
+  let x ← match x with | `([hvl_expr|$x]) => `(hvl_expr|$x) | _ => `(hvl_expr|@$x)
+  match op with
+    | `(UnOp.Not) => `([hvl_expr|!$x])
+    | `(UnOp.Non) => `([hvl_expr|~$x])
+    | `(UnOp.Iverson) => `([hvl_expr|[$x]])
+    | `(UnOp.Parens) => `([hvl_expr|($x)])
+    | _ => throw ()
+| _ => throw ()
+
+/-- info: [hvl_expr|!b + x * x + inf x: Int. (x + y)] -/
+#guard_msgs in
+#eval [hvl_expr|!b + x * x + inf x : Int. (x + y)]
+
+/-- info: fun b ↦ [hvl_expr|!@b] : Expr → Expr -/
+#guard_msgs in
+#check fun b ↦ [hvl_expr|!@b]
+
+open Lean in
+@[app_unexpander Caesar.Expr.DeBruijn]
+def Expr.unexpandDeBruijn : Unexpander
+| `($(_) {index:=$n:num}) =>
+  let name := s!"𝒹{Nat.toSubscriptString n.getNat}"
+  let name := mkIdent $ Name.mkSimple name
+  `([hvl_expr|$name:ident])
+| _ => throw ()
+
+/-- info: [hvl_expr|𝒹₀] -/
+#guard_msgs in
+#eval Expr.DeBruijn 0
+
+end Caesar
diff --git a/lean/Main.lean b/lean/Main.lean
new file mode 100644
index 00000000..c9d0f9d0
--- /dev/null
+++ b/lean/Main.lean
@@ -0,0 +1,4 @@
+import «Caesar»
+
+def main : IO Unit :=
+  IO.println s!"Hello, {hello}!"
diff --git a/lean/lake-manifest.json b/lean/lake-manifest.json
new file mode 100644
index 00000000..a67b19b2
--- /dev/null
+++ b/lean/lake-manifest.json
@@ -0,0 +1,95 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/leanprover-community/mathlib4.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "0eaf9c0dd6a851eb0fb447c605033c566246a733",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": null,
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "8cee626a680fe217814c4bd444b94ceb31efd6b6",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "8d29bc2c3ebe1f863c2f02df816b4f3dd1b65226",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "c20832d6f0b3186a97ea9361cec0a5b87dd152a3",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "ea953247aac573c9b5adea60bacd3e085f58aca4",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.56",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "57185dfad68d78356f9462af984882d6f262aa5d",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "aa4c87abed970d9dfad2506000d99d30b02f476b",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "f1a7afdb343196b33bf9137b232eb69446065925",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "aff4176e5c41737a0d73be74ad9feb6a889bfa98",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"}],
+ "name": "caesar",
+ "lakeDir": ".lake"}
diff --git a/lean/lakefile.lean b/lean/lakefile.lean
new file mode 100644
index 00000000..21c93514
--- /dev/null
+++ b/lean/lakefile.lean
@@ -0,0 +1,19 @@
+import Lake
+open Lake DSL
+
+package «caesar» where
+  -- add package configuration options here
+  leanOptions := #[
+    ⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b`
+    ⟨`pp.proofs.withType, false⟩
+  ]
+
+lean_lib «Caesar» where
+  -- add library configuration options here
+
+@[default_target]
+lean_exe «caesar» where
+  root := `Main
+
+require mathlib from git
+  "https://github.com/leanprover-community/mathlib4.git"
diff --git a/lean/lean-toolchain b/lean/lean-toolchain
new file mode 100644
index 00000000..c7e245cc
--- /dev/null
+++ b/lean/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.19.0-rc2
\ No newline at end of file