diff --git a/Lampe/Lampe.lean b/Lampe/Lampe.lean
index 90dc9f0..e114914 100644
--- a/Lampe/Lampe.lean
+++ b/Lampe/Lampe.lean
@@ -21,7 +21,8 @@ nr_def weirdEq<I>(x : I, y : I) -> Unit {
   #assert(#fEq(a, y) : bool) : Unit;
 }
 
-example {x y : Tp.denote p .field} : STHoare p Γ ⟦⟧ (weirdEq.fn.body _ h![.field] |>.body h![x, y]) fun _ => x = y := by
+example {x y : Tp.denote p .field} :
+  STHoare p Γ ⟦⟧ (weirdEq.fn.body _ h![.field] |>.body h![x, y]) fun _ => x = y := by
   simp only [weirdEq]
   steps
   simp_all
@@ -34,12 +35,15 @@ nr_def sliceAppend<I>(x: [I], y: [I]) -> [I] {
   self
 }
 
-lemma BitVec.add_toNat_of_lt_max {a b : BitVec w} (h: a.toNat + b.toNat < 2^w) : (a + b).toNat = a.toNat + b.toNat := by
+lemma BitVec.add_toNat_of_lt_max {a b : BitVec w} (h: a.toNat + b.toNat < 2^w) :
+    (a + b).toNat = a.toNat + b.toNat := by
   simp only [BitVec.add_def, BitVec.toNat_ofNat]
   rw [Nat.mod_eq_of_lt]
   assumption
 
-example {self that : Tp.denote p (.slice tp)} : STHoare p Γ ⟦⟧ (sliceAppend.fn.body _ h![tp] |>.body h![self, that]) fun v => v = self ++ that := by
+example {self that : Tp.denote p (.slice tp)} :
+    STHoare p Γ ⟦⟧ (sliceAppend.fn.body _ h![tp] |>.body h![self, that])
+    fun v => v = self ++ that := by
   simp only [sliceAppend]
   steps
   rename Tp.denote _ tp.slice.ref => selfRef
@@ -66,8 +70,8 @@ nr_def simple_if<>(x : Field, y : Field) -> Field {
   z
 }
 
-example {p Γ x y}: STHoare p Γ ⟦⟧ (simple_if.fn.body _ h![] |>.body h![x, y])
-  fun v => v = y := by
+example {p Γ x y} : STHoare p Γ ⟦⟧ (simple_if.fn.body _ h![] |>.body h![x, y])
+    fun v => v = y := by
   simp only [simple_if]
   steps <;> tauto
   . sl
@@ -82,35 +86,43 @@ nr_def simple_if_else<>(x : Field, y : Field) -> Field {
   z
 }
 
-example {p Γ x y}: STHoare p Γ ⟦⟧ (simple_if_else.fn.body _ h![] |>.body h![x, y])
-  fun v => v = x := by
+example {p Γ x y} : STHoare p Γ ⟦⟧ (simple_if_else.fn.body _ h![] |>.body h![x, y])
+    fun v => v = x := by
   simp only [simple_if_else]
   steps
   . simp only [decide_True, exists_const]
     sl
     contradiction
-  . aesop
+  . simp_all [decide_True, exists_const]
 
 nr_def simple_lambda<>(x : Field, y : Field) -> Field {
   let add = |a : Field, b : Field| -> Field { #fAdd(a, b) : Field };
-  ^add(x, y) : Field;
+  add(x, y);
 }
 
 example {p Γ} {x y : Tp.denote p Tp.field} :
-  STHoare p Γ ⟦⟧ (simple_lambda.fn.body _ h![] |>.body h![x, y])
-  fun v => v = (x + y) := by
+    STHoare p Γ ⟦⟧ (simple_lambda.fn.body _ h![] |>.body h![x, y])
+    fun v => v = x + y := by
   simp only [simple_lambda]
   steps
+  . apply STHoare.consequence_frame_left STHoare.callLambda_intro
+    . rw [SLP.star_assoc, SLP.star_comm, SLP.star_assoc]
+      rw [SLP.top_star_top]
+      apply SLP.ent_star_top
+    . exact fun v => v = x + y
+    . simp only
+      steps
+      simp_all only [exists_const, SLP.true_star]
+      unfold SLP.wand SLP.entails SLP.forall'
+      intros _ _ _ _ _ _
+      simp_all [SLP.star, SLP.lift]
   simp_all
   steps
   simp_all
-  rotate_left 2
-  simp_all [SLP.entails_self]
-  exact (fun v => v = x + y)
-  sl
-  aesop
-  sl
-  aesop
+  intros st₁ h₁ v st₂ _ _
+  apply SLP.ent_drop_left at h₁
+  unfold SLP.lift SLP.star at *
+  simp_all
 
 nr_trait_impl[bulbulizeField] <> Bulbulize<> for Field where {
     fn bulbulize<>(x : Field) -> Field {
@@ -129,73 +141,32 @@ def simpleTraitEnv : Env := {
   traits := [bulbulizeField, bulbulizeU32]
 }
 
-def simple_trait_call (tp : Tp) (arg : tp.denote P): Expr (Tp.denote P) tp :=
-  @Expr.call _ [] h![] [tp] tp (.trait ⟨⟨⟨"Bulbulize", [], h![]⟩, tp⟩, "bulbulize"⟩) h![arg]
-
-
-example : STHoare p simpleTraitEnv ⟦⟧ (simple_trait_call .field arg) (fun v => v = 2 * arg) := by
-  simp only [simple_trait_call]
-  steps
-  apply_impl [] bulbulizeField.2
-  tauto
-  any_goals rfl
-  simp only
-  steps
-  casesm ∃_, _
-  intro
-  subst_vars
-  ring
-
-example : STHoare p simpleTraitEnv ⟦⟧ (simple_trait_call (.u 32) arg) (fun v => v = 69) := by
-  simp only [simple_trait_call]
-  steps
-  apply_impl [] bulbulizeU32.2
-  tauto
-  any_goals rfl
-  simp only
-  steps
-  aesop
-
-
-example : STHoare p simpleTraitEnv ⟦⟧ (simple_trait_call (.u 32) arg) (fun v => v = 69) := by
-  simp only [simple_trait_call]
-  steps
-  try_impls [] [bulbulizeField.2, bulbulizeU32.2]
-  tauto
-  any_goals rfl
-  simp only
-  steps
-  aesop
-
-example : STHoare p simpleTraitEnv ⟦⟧ (simple_trait_call (.u 32) arg) (fun v => v = 69) := by
-  simp only [simple_trait_call]
-  steps
-  try_impls_all [] simpleTraitEnv
-  tauto
-  any_goals rfl
-  simp only
-  steps
-  aesop
-
-
-nr_def simple_trait_call_syntax<I> (x : I) -> I {
-  (I as Bulbulize<>)::bulbulize<>(x : I) : I
+nr_def simple_trait_call<I> (x : I) -> I {
+  ((I as Bulbulize<>)::bulbulize<> as λ(I) → I)(x)
 }
 
 example {p} {arg : Tp.denote p Tp.field} :
-  STHoare p simpleTraitEnv ⟦⟧ (simple_trait_call_syntax.fn.body _ h![.field] |>.body h![arg]) (fun v => v = 2 * arg) := by
-  simp only [simple_trait_call_syntax]
+    STHoare p simpleTraitEnv ⟦⟧ (simple_trait_call.fn.body _ h![.field] |>.body h![arg])
+    fun v => v = 2 * arg := by
+  simp only [simple_trait_call]
   steps
-  try_impls_all [] simpleTraitEnv
-  tauto
-  any_goals rfl
-  simp only
+  . apply STHoare.callTrait_intro
+    sl
+    tauto
+    try_impls_all [] simpleTraitEnv
+    all_goals tauto
+    simp only
+    steps
+    simp_all only [exists_const, SLP.true_star]
+    on_goal 2 => exact (fun v => v = 2 * arg)
+    sl
+    intros
+    subst_vars
+    ring
   steps
-  simp_all
-  rotate_left 1
-  all_goals try exact (fun v => v = 2 * arg)
-  all_goals (sl; intro; subst_vars; ring)
-
+  intros
+  subst_vars
+  rfl
 
 nr_trait_impl[me] <I> Me<> for I where {
     fn me<>(x : I) -> I {
@@ -209,20 +180,23 @@ def genericTraitEnv : Env := {
 }
 
 nr_def generic_trait_call<>(x : Field) -> Field {
-  (Field as Me<>)::me<>(x : Field) : Field
+  ((Field as Me<>)::me<> as λ(Field) → Field)(x)
 }
 
 example {p} {x : Tp.denote p Tp.field} :
-  STHoare p genericTraitEnv ⟦⟧ (generic_trait_call.fn.body _ h![] |>.body h![x]) (fun v => v = x) := by
+    STHoare p genericTraitEnv ⟦⟧ (generic_trait_call.fn.body _ h![] |>.body h![x])
+    fun v => v = x := by
   simp only [generic_trait_call]
   steps
-  try_impls_all [Tp.field] genericTraitEnv
-  tauto
-  all_goals try rfl
-  simp_all
-  steps
-  sl
-  aesop
+  . apply STHoare.callTrait_intro
+    sl
+    tauto
+    try_impls_all [Tp.field] genericTraitEnv
+    tauto
+    all_goals try rfl
+    steps
+  . steps
+    simp_all
 
 nr_struct_def Pair <I> {
   a : I,
@@ -234,7 +208,8 @@ nr_def struct_construct<>(a : Field, b : Field) -> Pair<Field> {
 }
 
 example {p} {a b : Tp.denote p .field} :
-  STHoare p Γ ⟦⟧ (struct_construct.fn.body _ h![] |>.body h![a, b]) (fun v => v.fst = a ∧ v.snd = (b, ())) := by
+    STHoare p Γ ⟦⟧ (struct_construct.fn.body _ h![] |>.body h![a, b])
+    fun v => v.fst = a ∧ v.snd = (b, ()) := by
   simp only [struct_construct]
   steps
   aesop
@@ -245,7 +220,8 @@ nr_def struct_project<>(x : Field, y : Field) -> Field {
 }
 
 example {p} {x y : Tp.denote p .field} :
-  STHoare p Γ ⟦⟧ (struct_project.fn.body _ h![] |>.body h![x, y]) (fun v => v = x) := by
+    STHoare p Γ ⟦⟧ (struct_project.fn.body _ h![] |>.body h![x, y])
+    fun v => v = x := by
   simp only [struct_project]
   steps
   aesop
@@ -255,39 +231,46 @@ nr_def basic_cast<>(x : u8) -> Field {
 }
 
 example {p} {x : Tp.denote p $ .u 8} :
-  STHoare p Γ ⟦⟧ (basic_cast.fn.body _ h![] |>.body h![x]) (fun (v : Tp.denote _ .field) => v = x.toNat) := by
+    STHoare p Γ ⟦⟧ (basic_cast.fn.body _ h![] |>.body h![x])
+    fun (v : Tp.denote p .field) => v = x.toNat := by
   simp only [basic_cast]
   steps
   aesop
 
-nr_def call_decl<>(x: Field, y : Field) -> Field {
-   let s = @struct_construct<>(x, y) : Pair<Field>;
-   (s as Pair<Field>).a
- }
+nr_def add_two_fields<>(a : Field, b : Field) -> Field {
+  #fAdd(a, b) : Field
+}
 
-example {x y : Tp.denote p .field} :
-  STHoare p ⟨[(struct_construct.name, struct_construct.fn)], []⟩
-    ⟦⟧ (call_decl.fn.body _ h![] |>.body h![x, y]) (fun v => v = x) := by
-  simp only [call_decl, struct_construct]
-  apply STHoare.letIn_intro
-  on_goal 3 => exact (fun (v : Tp.denote p $ .tuple _ [.field, .field]) => v = (x, y, ()))
-  apply STHoare.callDecl_intro <;> tauto
-  . apply STHoare.letIn_intro
-    . steps
-    . intros
-      steps
-      aesop
-  . intros
-    steps
-    aesop
+nr_def call_decl<>() -> Field {
+  (@add_two_fields<> as λ(Field, Field) → Field)(1 : Field, 2 : Field)
+}
 
+example : STHoare p ⟨[(add_two_fields.name, add_two_fields.fn)], []⟩ ⟦⟧
+    (call_decl.fn.body _ h![] |>.body h![])
+    fun (v : Tp.denote p .field) => v = 3 := by
+  simp only [call_decl]
+  steps
+  apply STHoare.callDecl_intro
+  . sl
+    tauto
+  on_goal 3 => exact add_two_fields.fn
+  all_goals tauto
+  on_goal 3 => exact fun v => v = 3
+  . simp only [add_two_fields]
+    steps
+    simp_all
+    intros
+    ring
+  . steps
+    simp_all
 
 nr_def simple_tuple<>() -> Field {
   let t = `(1 : Field, true, 3 : Field);
   t.2
 }
 
-example : STHoare p Γ ⟦⟧ (simple_tuple.fn.body _ h![] |>.body h![]) (fun (v : Tp.denote p .field) => v = 3) := by
+example : STHoare p Γ ⟦⟧ (simple_tuple.fn.body _ h![] |>.body h![])
+    fun (v : Tp.denote p .field) => v = 3 := by
   simp only [simple_tuple]
   steps
   aesop
@@ -297,16 +280,20 @@ nr_def simple_slice<>() -> bool {
   s[[1 : u32]]
 }
 
-example : STHoare p Γ ⟦⟧ (simple_slice.fn.body _ h![] |>.body h![]) (fun (v : Tp.denote p .bool) => v = false) := by
+example : STHoare p Γ ⟦⟧ (simple_slice.fn.body _ h![] |>.body h![])
+    fun (v : Tp.denote p .bool) => v = false := by
   simp only [simple_slice, Expr.mkSlice]
-  steps <;> aesop
+  steps
+  rfl
+  aesop
 
 nr_def simple_array<>() -> Field {
   let arr = [1 : Field, 2 : Field];
   arr[1 : u32]
 }
 
-example : STHoare p Γ ⟦⟧ (simple_array.fn.body _ h![] |>.body h![]) (fun (v : Tp.denote p .field) => v = 2) := by
+example : STHoare p Γ ⟦⟧ (simple_array.fn.body _ h![] |>.body h![])
+    fun (v : Tp.denote p .field) => v = 2 := by
   simp only [simple_array, Expr.mkArray]
   steps <;> tauto
   aesop
@@ -317,10 +304,15 @@ nr_def tuple_lens<>() -> Field {
   p .0 .1
 }
 
-example : STHoare p Γ ⟦⟧ (tuple_lens.fn.body _ h![] |>.body h![]) fun (v : Tp.denote p .field) => v = 3 := by
+example : STHoare p Γ ⟦⟧ (tuple_lens.fn.body _ h![] |>.body h![])
+    fun (v : Tp.denote p .field) => v = 3 := by
   simp only [tuple_lens]
   steps
-  aesop
+  subst_vars
+  simp_all only [Access.get, exists_const, Lens.modify, Lens.get, Option.bind_eq_bind,
+    Option.some_bind, Option.bind_some, Option.some.injEq]
+  subst_vars
+  rfl
 
 nr_def struct_lens<>() -> Field {
   let mut p = `(Pair<Field>{ 1 : Field, 2 : Field}, 3 : Field);
@@ -328,7 +320,8 @@ nr_def struct_lens<>() -> Field {
   (p .0 as Pair<Field>).b
 }
 
-example : STHoare p Γ ⟦⟧ (struct_lens.fn.body _ h![] |>.body h![]) fun (v : Tp.denote p .field) => v = 3 := by
+example : STHoare p Γ ⟦⟧ (struct_lens.fn.body _ h![] |>.body h![])
+    fun (v : Tp.denote p .field) => v = 3 := by
   simp only [struct_lens]
   steps
   aesop
@@ -339,7 +332,8 @@ nr_def array_lens<>() -> Field {
   p.0[1 : u32]
 }
 
-example : STHoare p Γ ⟦⟧ (array_lens.fn.body _ h![] |>.body h![]) fun (v : Tp.denote p .field) => v = 3 := by
+example : STHoare p Γ ⟦⟧ (array_lens.fn.body _ h![] |>.body h![])
+    fun (v : Tp.denote p .field) => v = 3 := by
   simp only [array_lens]
   steps
   rfl
@@ -355,7 +349,8 @@ nr_def slice_lens<>() -> Field {
   p .0 [[1 : u32]]
 }
 
-example : STHoare p Γ ⟦⟧ (slice_lens.fn.body _ h![] |>.body h![]) fun (v : Tp.denote p .field) => v = 3 := by
+example : STHoare p Γ ⟦⟧ (slice_lens.fn.body _ h![] |>.body h![])
+    fun (v : Tp.denote p .field) => v = 3 := by
   simp only [slice_lens]
   steps
   all_goals try exact ([1, 3], 3)
@@ -363,3 +358,41 @@ example : STHoare p Γ ⟦⟧ (slice_lens.fn.body _ h![] |>.body h![]) fun (v :
   . simp_all
     rfl
   . simp_all [Builtin.indexTpl]
+
+nr_def simple_func<>() -> Field {
+  10 : Field
+}
+
+nr_def call<>(f : λ() → Field) -> Field {
+  f()
+}
+
+nr_def simple_hof<>() -> Field {
+  let func = @simple_func<> as λ() → Field;
+  (@call<> as λ(λ() → Field) → Field)(func)
+}
+
+example : STHoare p ⟨[(simple_func.name, simple_func.fn), (call.name, call.fn)], []⟩ ⟦⟧
+    (simple_hof.fn.body _ h![] |>.body h![])
+    fun (v : Tp.denote p .field) => v = 10 := by
+  simp only [simple_hof]
+  steps
+  . apply STHoare.callDecl_intro
+    sl
+    all_goals tauto
+    simp only [call]
+    steps
+    . apply STHoare.callDecl_intro
+      sl
+      all_goals tauto
+      simp only [simple_func]
+      steps
+      on_goal 2 => exact fun v => v = 10
+      sl
+      simp_all
+    . steps
+      on_goal 2 => exact fun v => v = 10
+      sl
+      simp_all
+  steps
+  simp_all
diff --git a/Lampe/Lampe/Ast.lean b/Lampe/Lampe/Ast.lean
index fb62b94..a620020 100644
--- a/Lampe/Lampe/Ast.lean
+++ b/Lampe/Lampe/Ast.lean
@@ -9,9 +9,6 @@ namespace Lampe
 
 abbrev Ident := String
 
-/-- A reference to a lambda is represented as a reference to a unit type -/
-abbrev Tp.lambdaRef := Tp.ref .unit
-
 structure TraitRef where
   name : Ident
   traitGenericKinds : List Kind
@@ -25,21 +22,17 @@ structure TraitMethodImplRef where
   trait : TraitImplRef
   method : Ident
 
-inductive FunctionIdent (rep : Tp → Type) : Type where
-| builtin : Builtin → FunctionIdent rep
-| decl : Ident → FunctionIdent rep
-| lambda : rep .lambdaRef → FunctionIdent rep
-| trait : TraitMethodImplRef → FunctionIdent rep
-
 inductive Expr (rep : Tp → Type) : Tp → Type where
 | lit : (tp : Tp) → Nat → Expr rep tp
+| fn : (argTps : List Tp) → (outTp : Tp) → (r : FuncRef argTps outTp) → Expr rep (.fn argTps outTp)
 | var : rep tp → Expr rep tp
 | letIn : Expr rep t₁ → (rep t₁ → Expr rep t₂) → Expr rep t₂
-| call : HList Kind.denote tyKinds → (argTypes : List Tp) → (res : Tp) → FunctionIdent rep → HList rep argTypes → Expr rep res
+| call : (argTps : List Tp) → (outTp : Tp) → (rep $ .fn argTps outTp) → (args : HList rep argTps) → Expr rep outTp
+| callBuiltin : (argTps : List Tp) → (outTp : Tp) → (b : Builtin) → (args : HList rep argTps) → Expr rep outTp
 | ite : rep .bool → Expr rep a → Expr rep a → Expr rep a
 | skip : Expr rep .unit
 | loop : rep (.u s) → rep (.u s) → (rep (.u s) → Expr rep r) → Expr rep .unit
-| lambda : (argTps : List Tp) → (outTp : Tp) → (HList rep argTps → Expr rep outTp) → Expr rep .lambdaRef
+| lam : (argTps : List Tp) → (outTp : Tp) → (HList rep argTps → Expr rep outTp) → Expr rep (.fn argTps outTp)
 
 structure Lambda (rep : Tp → Type) where
   argTps : List Tp
diff --git a/Lampe/Lampe/Hoare/Builtins.lean b/Lampe/Lampe/Hoare/Builtins.lean
index 5cd3344..044d9b3 100644
--- a/Lampe/Lampe/Hoare/Builtins.lean
+++ b/Lampe/Lampe/Hoare/Builtins.lean
@@ -21,7 +21,7 @@ Introduction rule for pure builtins.
 theorem pureBuiltin_intro {A : Type} {a : A} {sgn desc args} :
   STHoare p Γ
     ⟦⟧
-    (.call h![] (sgn a).fst (sgn a).snd (.builtin (Builtin.newGenericPureBuiltin sgn desc)) args)
+    (.callBuiltin (sgn a).fst (sgn a).snd (Builtin.newGenericPureBuiltin sgn desc) args)
     (fun v => ∃h, (v = (desc a args).snd h)) := by
   unfold STHoare
   intro H
@@ -44,7 +44,7 @@ lemma pureBuiltin_intro_consequence
     (h2 : outTp = (sgn a).snd)
     (hp : (h: (desc a (h1 ▸ args)).fst) → Q (h2 ▸ (desc a (h1 ▸ args)).snd h)) :
     STHoare p Γ ⟦⟧
-      (.call h![] argTps outTp (.builtin (Builtin.newGenericPureBuiltin sgn desc)) args)
+      (.callBuiltin argTps outTp (Builtin.newGenericPureBuiltin sgn desc) args)
       fun v => Q v := by
   subst_vars
   dsimp only at *
@@ -369,7 +369,7 @@ theorem strAsBytes_intro : STHoarePureBuiltin p Γ Builtin.strAsBytes (by tauto)
 theorem ref_intro :
     STHoare p Γ
       ⟦⟧
-      (.call h![] [tp] (Tp.ref tp) (.builtin .ref) h![v])
+      (.callBuiltin [tp] (.ref tp) .ref h![v])
       (fun r => [r ↦ ⟨tp, v⟩]) := by
   unfold STHoare
   intro H
@@ -393,7 +393,7 @@ theorem ref_intro :
 theorem readRef_intro :
     STHoare p Γ
     [r ↦ ⟨tp, v⟩]
-    (.call h![] [tp.ref] tp (.builtin .readRef) h![r])
+    (.callBuiltin [.ref tp] tp .readRef h![r])
     (fun v' => ⟦v' = v⟧ ⋆ [r ↦ ⟨tp, v⟩]) := by
   unfold STHoare
   intro H
@@ -426,7 +426,7 @@ theorem readRef_intro :
 theorem writeRef_intro :
     STHoare p Γ
     [r ↦ ⟨tp, v⟩]
-    (.call h![] [tp.ref, tp] .unit (.builtin .writeRef) h![r, v'])
+    (.callBuiltin [.ref tp, tp] .unit .writeRef h![r, v'])
     (fun _ => [r ↦ ⟨tp, v'⟩]) := by
   unfold STHoare
   intro H
@@ -471,7 +471,7 @@ theorem projectTuple_intro : STHoarePureBuiltin p Γ (Builtin.projectTuple mem)
 theorem readLens_intro {lens : Lens (Tp.denote p) tp₁ tp₂} :
     STHoare p Γ
     [r ↦ ⟨tp₁, s⟩]
-    (.call h![] [tp₁.ref] tp₂ (.builtin $ .readLens lens) h![r])
+    (.callBuiltin [tp₁.ref] tp₂ (.readLens lens) h![r])
     (fun v' => ⟦lens.get s = some v'⟧ ⋆ [r ↦ ⟨tp₁, s⟩]) := by
   unfold STHoare THoare
   intros H st h
@@ -491,7 +491,7 @@ theorem readLens_intro {lens : Lens (Tp.denote p) tp₁ tp₂} :
  theorem modifyLens_intro {lens : Lens (Tp.denote p) tp₁ tp₂} {s : Tp.denote p tp₁} {v : Tp.denote p tp₂} :
     STHoare p Γ
     [r ↦ ⟨tp₁, s⟩]
-    (.call h![] [tp₁.ref, tp₂] .unit (.builtin $ .modifyLens lens) h![r, v])
+    (.callBuiltin [tp₁.ref, tp₂] .unit (.modifyLens lens) h![r, v])
     (fun _ => ∃∃h, [r ↦ ⟨tp₁, lens.modify s v |>.get h⟩]) := by
   unfold STHoare THoare
   intros H st h
@@ -528,7 +528,7 @@ theorem readLens_intro {lens : Lens (Tp.denote p) tp₁ tp₂} :
 theorem getLens_intro {lens : Lens (Tp.denote p) tp₁ tp₂} :
     STHoare p Γ
     ⟦⟧
-    (.call h![] [tp₁] tp₂ (.builtin $ .getLens lens) h![s])
+    (.callBuiltin [tp₁] tp₂ (.getLens lens) h![s])
     (fun v => ⟦lens.get s = some v⟧) := by
   unfold STHoare THoare
   intros H st h
@@ -547,7 +547,7 @@ theorem assert_intro : STHoarePureBuiltin p Γ Builtin.assert (by tauto) h![a] (
   apply pureBuiltin_intro_consequence <;> tauto
   tauto
 
-theorem cast_intro [Builtin.CastTp tp tp'] : STHoare p Γ ⟦⟧ (.call h![] [tp] tp' (.builtin .cast) h![v])
+theorem cast_intro [Builtin.CastTp tp tp'] : STHoare p Γ ⟦⟧ (.callBuiltin [tp] tp' .cast h![v])
    (fun v' => ∃∃ h, ⟦@Builtin.CastTp.cast tp tp' _ p v h = v'⟧) := by
    unfold STHoare THoare
    intros
diff --git a/Lampe/Lampe/Hoare/SepTotal.lean b/Lampe/Lampe/Hoare/SepTotal.lean
index 1f202af..08fb103 100644
--- a/Lampe/Lampe/Hoare/SepTotal.lean
+++ b/Lampe/Lampe/Hoare/SepTotal.lean
@@ -30,7 +30,7 @@ abbrev STHoarePureBuiltin p (Γ : Env)
   (_ : b = @Builtin.newGenericPureBuiltin A sgn desc)
   (args : HList (Tp.denote p) (sgn a).fst) : Prop :=
     STHoare p Γ ⟦⟧
-      (.call h![] (sgn a).fst (sgn a).snd (.builtin b) args)
+      (.callBuiltin (sgn a).fst (sgn a).snd b args)
       (fun v => ∃h, v = (desc a (args)).snd h)
 
 namespace STHoare
@@ -133,7 +133,7 @@ lemma Finmap.union_singleton [DecidableEq α] {β : α → Type u} {r : α} {v v
 theorem fresh_intro :
   STHoare p Γ
       ⟦⟧
-      (.call h![] [] tp (.builtin .fresh) h![])
+      (.callBuiltin [] tp .fresh h![])
       (fun _ => ⟦⟧) := by
   unfold STHoare
   intro H
@@ -306,42 +306,9 @@ theorem skip_intro :
   . apply SLP.ent_star_top
     tauto
 
-theorem callLambda_intro {lambdaBody} {P : SLP (State p)} {Q : Tp.denote p outTp → SLP (State p)}:
-  @STHoare outTp p Γ P (lambdaBody args) Q →
-  STHoare p Γ (P ⋆ [λref ↦ ⟨argTps, outTp, lambdaBody⟩])
-    (Expr.call h![] argTps outTp (.lambda ref) args)
-    (fun v => (Q v) ⋆ [λref ↦ ⟨argTps, outTp, lambdaBody⟩]) := by
-  intros
-  rename_i h
-  unfold STHoare THoare
-  intros
-  constructor <;> tauto
-  unfold SLP.star at *
-  . rename_i st h
-    obtain ⟨st₁, ⟨st₂, ⟨_, h₂, h₃, _⟩⟩⟩ := h
-    obtain ⟨st₁', ⟨st₂', _⟩⟩ := h₃
-    simp_all only [State.union_parts, Finmap.mem_union, Finmap.mem_singleton, or_true,
-      Finmap.lookup_union_left]
-    generalize hL : (⟨_, _, _⟩ : Lambda _) = lmb at *
-    have _ : ref ∉ st₁'.lambdas := by
-      rename_i h₃
-      obtain ⟨hi₁, _, _, hi₂⟩ := h₃
-      simp only [State.lmbSingleton] at hi₂
-      simp only [LawfulHeap.disjoint] at hi₁
-      obtain ⟨_, hj₁⟩ := hi₁
-      rw [hi₂] at hj₁
-      tauto
-    simp [Finmap.lookup_union_right (by tauto)]
-  . apply consequence <;> tauto
-    apply consequence_frame_left
-    rotate_left 2
-    exact P
-    exact h
-    simp only [SLP.true_star, SLP.entails_self]
-
 theorem lam_intro :
-  STHoare p Γ ⟦⟧ (.lambda argTps outTp lambdaBody)
-    fun v => [λv ↦ ⟨argTps, outTp, lambdaBody⟩] := by
+  STHoare p Γ ⟦⟧ (.lam argTps outTp lambdaBody)
+    fun v => ∃∃ r, ⟦v = FuncRef.lambda r⟧ ⋆ [λr ↦ ⟨argTps, outTp, lambdaBody⟩] := by
   unfold STHoare THoare
   intros H st h
   constructor
@@ -361,38 +328,81 @@ theorem lam_intro :
       rw [Finmap.Disjoint.symm_iff]
       apply Finmap.singleton_disjoint_of_not_mem (by assumption)
     simp only [Finmap.insert_eq_singleton_union, Finmap.union_comm_of_disjoint hd]
-  . unfold State.lmbSingleton
-    tauto
+  . unfold State.lmbSingleton SLP.exists'
+    exists r
+    simp_all only [SLP.true_star]
   . apply SLP.ent_star_top
     tauto
 
-theorem callTrait_intro {impl} {fname fn}
-    (h_trait : TraitResolution Γ traitRef impl)
-    (h_fn : (fname, fn) ∈ impl)
-    (hkc : fn.generics = tyKinds)
-    (htci : (fn.body _ (hkc ▸ generics) |>.argTps) = argTypes)
-    (htco : (fn.body _ (hkc ▸ generics) |>.outTp) = res)
-    (h_hoare: STHoare p Γ H (htco ▸ (fn.body _ (hkc ▸ generics) |>.body (htci ▸ args))) Q):
+theorem callLambda_intro {lambdaBody} {P : SLP $ State p}
+  {Q : Tp.denote p outTp → SLP (State p)}
+  {fnRef : Tp.denote p (.fn argTps outTp)}
+  {hlam : STHoare p Γ P (lambdaBody args) Q} :
+  STHoare p Γ (P ⋆ ∃∃ r, ⟦fnRef = FuncRef.lambda r⟧ ⋆ [λr ↦ ⟨argTps, outTp, lambdaBody⟩])
+    (Expr.call argTps outTp fnRef args)
+    (fun v => (Q v) ⋆ ∃∃ r, ⟦fnRef = FuncRef.lambda r⟧ ⋆ [λr ↦ ⟨argTps, outTp, lambdaBody⟩]) := by
+  unfold STHoare THoare
+  intros H st h
+  have h₁ : ∃ r, fnRef = .lambda r := by
+    simp only [SLP.star, SLP.exists', SLP.lift] at h
+    tauto
+  obtain ⟨r, _⟩ := h₁
+  apply Omni.callLambda <;> tauto
+  . obtain ⟨st₁, st₂, _, _, ⟨_, _, _, _, _, _, _, _, _, _, ⟨_, _⟩, _⟩, _⟩ := h
+    subst_vars
+    simp_all only [FuncRef.lambda.injEq]
+    subst_vars
+    simp_all only [LawfulHeap.empty_union, LawfulHeap.empty_disjoint]
+    simp only [State.union_parts]
+    rw [Finmap.lookup_union_left, Finmap.lookup_union_right]
+    <;> simp only [State.lmbSingleton, LawfulHeap.disjoint, State.union_parts] at *
+    . simp_all
+    . apply Finmap.singleton_disjoint_iff_not_mem.mp
+      simp_all only
+      tauto
+    . simp_all
+  apply STHoare.consequence_frame_left <;> tauto
+
+theorem callDecl_intro {fnRef : Tp.denote p (.fn argTps outTp)}
+    {href : H ⊢ ⟦fnRef = (.decl fnName kinds generics)⟧ ⋆ (⊤ : SLP $ State p)}
+    {h_fn : (fnName, fn) ∈ Γ.functions}
+    {hkc : fn.generics = kinds}
+    {htci : (fn.body _ (hkc ▸ generics) |>.argTps) = argTps}
+    {htco : (fn.body _ (hkc ▸ generics) |>.outTp) = outTp}
+    {h_hoare: STHoare p Γ H (htco ▸ (fn.body _ (hkc ▸ generics) |>.body (htci ▸ args))) Q} :
+    STHoare p Γ H (Expr.call argTps outTp fnRef args) Q := by
+  unfold STHoare THoare
+  intros
+  have _ : fnRef = (.decl fnName kinds generics) := by
+    rename_i h'
+    apply SLP.extract_prop at h' <;> tauto
+  apply Omni.callDecl <;> tauto
+
+
+theorem callTrait_intro {impls : List $ Ident × Function} {fnRef : Tp.denote p (.fn argTps outTp)}
+    (href : H ⊢  ⟦fnRef = (.trait selfTp traitName traitKinds traitGenerics fnName kinds generics)⟧ ⋆ (⊤ : SLP $ State p))
+    (h_trait : TraitResolution Γ ⟨⟨traitName, traitKinds, traitGenerics⟩, selfTp⟩ impls)
+    (h_fn : (fnName, fn) ∈ impls)
+    (hkc : fn.generics = kinds)
+    (htci : (fn.body _ (hkc ▸ generics) |>.argTps) = argTps)
+    (htco : (fn.body _ (hkc ▸ generics) |>.outTp) = outTp)
+    (h_hoare: STHoare p Γ H (htco ▸ (fn.body _ (hkc ▸ generics) |>.body (htci ▸ args))) Q) :
     STHoare p Γ H
-      (@Expr.call _ tyKinds generics argTypes res (.trait ⟨traitRef, fname⟩) args)
+      (Expr.call argTps outTp fnRef args)
       Q := by
   unfold STHoare THoare
   intros
-  apply Omni.callTrait <;> try assumption
-  apply_assumption
-  assumption
+  have _ : fnRef = (.trait selfTp traitName traitKinds traitGenerics fnName kinds generics) := by
+    rename_i h'
+    apply SLP.extract_prop at h' <;> tauto
+  apply Omni.callTrait <;> tauto
 
-theorem callDecl_intro {fname fn}
-     (h_fn : (fname, fn) ∈ Γ.functions)
-     (hkc : fn.generics = tyKinds)
-     (htci : (fn.body _ (hkc ▸ generics) |>.argTps) = argTps)
-     (htco : (fn.body _ (hkc ▸ generics) |>.outTp) = res)
-     (h_hoare: STHoare p Γ H (htco ▸ (fn.body _ (hkc ▸ generics) |>.body (htci ▸ args))) Q):
-     STHoare p Γ H
-       (@Expr.call _ tyKinds generics argTps res (.decl fname) args)
-       Q := by
-   unfold STHoare THoare
-   intros
-   apply Omni.callDecl <;> tauto
+theorem fn_intro : STHoare p Γ ⟦⟧ (.fn argTps outTp r) fun v => v = r := by
+  unfold STHoare THoare
+  intro H st hp
+  constructor
+  simp only
+  apply SLP.ent_star_top
+  assumption
 
 end Lampe.STHoare
diff --git a/Lampe/Lampe/Hoare/Total.lean b/Lampe/Lampe/Hoare/Total.lean
index 32b75a7..4578aeb 100644
--- a/Lampe/Lampe/Hoare/Total.lean
+++ b/Lampe/Lampe/Hoare/Total.lean
@@ -45,7 +45,7 @@ theorem letIn_intro {P Q}
 theorem ref_intro {v P} :
     THoare p Γ
       (fun st => ∀r, r ∉ st → P r ⟨(st.vals.insert r ⟨tp, v⟩), st.lambdas⟩)
-      (.call h![] [tp] (Tp.ref tp) (.builtin .ref) h![v])
+      (.callBuiltin [tp] (.ref tp) .ref h![v])
       P := by
   unfold THoare
   intros
@@ -56,7 +56,7 @@ theorem ref_intro {v P} :
 theorem readRef_intro {ref} :
     THoare p Γ
       (fun st => st.vals.lookup ref = some ⟨tp, v⟩ ∧ P v st)
-      (.call h![] [tp.ref] tp (.builtin .readRef) h![ref])
+      (.callBuiltin [.ref tp] tp .readRef h![ref])
       P := by
   unfold THoare
   intros
@@ -66,7 +66,7 @@ theorem readRef_intro {ref} :
 theorem writeRef_intro {ref v} :
     THoare p Γ
       (fun st => ref ∈ st ∧ P () ⟨(st.vals.insert ref ⟨tp, v⟩), st.lambdas⟩)
-      (.call h![] [tp.ref, tp] .unit (.builtin .writeRef) h![ref, v])
+      (.callBuiltin [.ref tp, tp] .unit .writeRef h![ref, v])
       P := by
   unfold THoare
   intros
@@ -76,7 +76,7 @@ theorem writeRef_intro {ref v} :
 theorem fresh_intro {P} :
     THoare p Γ
       (∀∀v, P v)
-      (.call h![] [] tp (.builtin .fresh) h![])
+      (.callBuiltin [] tp .fresh h![])
       P := by
   unfold THoare
   intro st h
diff --git a/Lampe/Lampe/Semantics.lean b/Lampe/Lampe/Semantics.lean
index 7524970..25b2e33 100644
--- a/Lampe/Lampe/Semantics.lean
+++ b/Lampe/Lampe/Semantics.lean
@@ -14,8 +14,8 @@ structure Env where
   functions : List (Ident × Function)
   traits : List (Ident × TraitImpl)
 
-inductive TraitResolvable (Γ : Env): TraitImplRef → Prop where
-| ok {ref impl}:
+inductive TraitResolvable (Γ : Env) : TraitImplRef → Prop where
+| ok {ref impl} :
   (ref.trait.name, impl) ∈ Γ.traits →
   (ktc : ref.trait.traitGenericKinds = impl.traitGenericKinds) →
   (implGenerics : HList Kind.denote impl.implGenericKinds) →
@@ -24,7 +24,7 @@ inductive TraitResolvable (Γ : Env): TraitImplRef → Prop where
   (∀constraint ∈ impl.constraints implGenerics, TraitResolvable Γ constraint) →
   TraitResolvable Γ ref
 
-inductive TraitResolution (Γ : Env): TraitImplRef → List (Ident × Function) → Prop where
+inductive TraitResolution (Γ : Env) : TraitImplRef → List (Ident × Function) → Prop where
 | ok {ref impl}
   (h_mem : (ref.trait.name, impl) ∈ Γ.traits)
   (ktc : ref.trait.traitGenericKinds = impl.traitGenericKinds)
@@ -40,6 +40,7 @@ inductive Omni : Env → State p → Expr (Tp.denote p) tp → (Option (State p
 | litTrue {Q} : Q (some (st, true)) → Omni Γ st (.lit .bool 1) Q
 | litRef {Q} : Q (some (st, ⟨r⟩)) → Omni Γ st (.lit (.ref tp) r) Q
 | litU {Q} : Q (some (st, ↑n)) → Omni Γ st (.lit (.u s) n) Q
+| fn {Q} : Q (some (st, r)) → Omni Γ st (.fn _ _ r) Q
 | var {Q} : Q (some (st, v)) → Omni Γ st (.var v) Q
 | skip {Q} : Q (some (st, ())) → Omni Γ st (.skip) Q
 | iteTrue {mainBranch elseBranch} :
@@ -53,31 +54,34 @@ inductive Omni : Env → State p → Expr (Tp.denote p) tp → (Option (State p
   (∀v st, Q₁ (some (st, v)) → Omni Γ st (b v) Q) →
   (Q₁ none → Q none) →
   Omni Γ st (.letIn e b) Q
-| callLambda {lambdas : Lambdas p} :
+| callTrait {fnRef} :
+  fnRef = (.trait selfTp traitName traitKinds traitGenerics fnName kinds generics) →
+  TraitResolution Γ ⟨⟨traitName, traitKinds, traitGenerics⟩, selfTp⟩ impls →
+  (fnName, fn) ∈ impls →
+  (hkc : fn.generics = kinds) →
+  (htci : (fn.body (Tp.denote p) (hkc ▸ generics) |>.argTps) = argTps) →
+  (htco : (fn.body (Tp.denote p) (hkc ▸ generics) |>.outTp) = outTp) →
+  Omni Γ ⟨vh, lambdas⟩ (htco ▸ (fn.body (Tp.denote p) (hkc ▸ generics) |>.body (htci ▸ args))) Q →
+  Omni Γ ⟨vh, lambdas⟩ (Expr.call argTps outTp fnRef args) Q
+| callLambda {fnRef} {lambdaBody : HList (Tp.denote p) argTps → Expr (Tp.denote p) outTp} :
+  fnRef = (.lambda ref) →
   lambdas.lookup ref = some ⟨argTps, outTp, lambdaBody⟩ →
   Omni Γ ⟨vh, lambdas⟩ (lambdaBody args) Q →
-  Omni Γ ⟨vh, lambdas⟩ (Expr.call h![] argTps outTp (.lambda ref) args) Q
+  Omni Γ ⟨vh, lambdas⟩ (Expr.call argTps outTp fnRef args) Q
+| callDecl {fnRef} :
+  fnRef = (.decl fnName kinds generics) →
+  (fnName, fn) ∈ Γ.functions →
+  (hkc : fn.generics = kinds) →
+  (htci : (fn.body (Tp.denote p) (hkc ▸ generics) |>.argTps) = argTps) →
+  (htco : (fn.body (Tp.denote p) (hkc ▸ generics) |>.outTp) = outTp) →
+  Omni Γ ⟨vh, lambdas⟩ (htco ▸ (fn.body (Tp.denote p) (hkc ▸ generics) |>.body (htci ▸ args))) Q →
+  Omni Γ ⟨vh, lambdas⟩ (Expr.call argTps outTp fnRef args) Q
 | lam {Q} :
-  (∀ ref, ref ∉ lambdas → Q (some (⟨vh, lambdas.insert ref ⟨argTps, outTp, lambdaBody⟩⟩, ref))) →
-  Omni Γ ⟨vh, lambdas⟩ (Expr.lambda argTps outTp lambdaBody) Q
+  (∀ ref, ref ∉ lambdas → Q (some (⟨vh, lambdas.insert ref ⟨argTps, outTp, lambdaBody⟩⟩, FuncRef.lambda ref))) →
+  Omni Γ ⟨vh, lambdas⟩ (Expr.lam argTps outTp lambdaBody) Q
 | callBuiltin {Q} :
-    (b.omni p st argTypes resType args (mapToValHeapCondition st.lambdas Q)) →
-    Omni Γ st (Expr.call h![] argTypes resType (.builtin b) args) Q
-| callDecl:
-    (fname, fn) ∈ Γ.functions →
-    (hkc : fn.generics = tyKinds) →
-    (htci : (fn.body _ (hkc ▸ generics) |>.argTps) = argTypes) →
-    (htco : (fn.body _ (hkc ▸ generics) |>.outTp) = res) →
-    Omni Γ st (htco ▸ (fn.body _ (hkc ▸ generics) |>.body (htci ▸ args))) Q →
-    Omni Γ st (@Expr.call _ tyKinds generics argTypes res (.decl fname) args) Q
-| callTrait {impl}:
-    TraitResolution Γ traitRef impl →
-    (fname, fn) ∈ impl →
-    (hkc : fn.generics = tyKinds) →
-    (htci : (fn.body _ (hkc ▸ generics) |>.argTps) = argTypes) →
-    (htco : (fn.body _ (hkc ▸ generics) |>.outTp) = res) →
-    Omni Γ st (htco ▸ (fn.body _ (hkc ▸ generics) |>.body (htci ▸ args))) Q →
-    Omni Γ st (@Expr.call (Tp.denote p) tyKinds generics argTypes res (.trait ⟨traitRef, fname⟩) args) Q
+  (b.omni p st argTps outTp args (mapToValHeapCondition st.lambdas Q)) →
+  Omni Γ st (Expr.callBuiltin argTps outTp b args) Q
 | loopDone :
   lo ≥ hi →
   Omni Γ st (.loop lo hi body) Q
@@ -86,27 +90,34 @@ inductive Omni : Env → State p → Expr (Tp.denote p) tp → (Option (State p
   Omni Γ st (.letIn (body lo) (fun _ => .loop (lo + 1) hi body)) Q →
   Omni Γ st (.loop lo hi body) Q
 
-theorem Omni.consequence {p Γ st tp} {e : Expr (Tp.denote p) tp} {Q Q'}:
+theorem Omni.consequence {p Γ st tp} {e : Expr (Tp.denote p) tp} {Q Q'} :
     Omni p Γ st e Q →
     (∀ v, Q v → Q' v) →
     Omni p Γ st e Q' := by
   intro h
-  induction h <;> try (
+  induction h with
+  | callDecl =>
     intro
-    constructor
-    all_goals tauto
-  )
-  case callBuiltin =>
+    apply Omni.callDecl <;> tauto
+  | callLambda =>
+    intro
+    apply Omni.callLambda <;> tauto
+  | callBuiltin =>
     cases_type Builtin
     intros
     constructor
     tauto
-  case loopNext =>
+  | loopNext =>
     intro
     apply loopNext (by assumption)
     tauto
+  | _ =>
+    intro
+    constructor
+    all_goals tauto
+
 
-theorem Omni.frame {p Γ tp} {st₁ st₂ : State p} {e : Expr (Tp.denote p) tp} {Q}:
+theorem Omni.frame {p Γ tp} {st₁ st₂ : State p} {e : Expr (Tp.denote p) tp} {Q} :
     Omni p Γ st₁ e Q →
     LawfulHeap.disjoint st₁ st₂ →
     Omni p Γ (st₁ ∪ st₂) e (fun stv => match stv with
@@ -116,11 +127,12 @@ theorem Omni.frame {p Γ tp} {st₁ st₂ : State p} {e : Expr (Tp.denote p) tp}
   intro h
   induction h with
   | litField hq
-  | skip hq
   | litFalse hq
   | litTrue hq
   | litU hq
   | litRef hq
+  | skip hq
+  | fn
   | var hq =>
     intro
     constructor
@@ -140,6 +152,21 @@ theorem Omni.frame {p Γ tp} {st₁ st₂ : State p} {e : Expr (Tp.denote p) tp}
       assumption
       assumption
     · simp_all
+  | callDecl =>
+    intro
+    apply Omni.callDecl <;> tauto
+  | callTrait =>
+    intro
+    apply Omni.callTrait <;> tauto
+  | callLambda h =>
+    intro hd
+    apply Omni.callLambda <;> try tauto
+    simp_all
+    simp only [LawfulHeap.disjoint] at hd
+    rw [Finmap.lookup_union_left]
+    tauto
+    rw [Finmap.mem_iff]
+    tauto
   | callBuiltin hq =>
     rename Builtin => b
     intros
@@ -183,16 +210,6 @@ theorem Omni.frame {p Γ tp} {st₁ st₂ : State p} {e : Expr (Tp.denote p) tp}
       . simp only [State.union_parts, State.mk.injEq]
         tauto
       . rw [hin₄]
-  | callDecl =>
-    intro
-    constructor
-    all_goals (try assumption)
-    tauto
-  | callTrait _ _ _ _ _ _ _ =>
-    intro
-    constructor
-    all_goals (try assumption)
-    tauto
   | loopDone =>
     intro
     constructor
@@ -207,13 +224,6 @@ theorem Omni.frame {p Γ tp} {st₁ st₂ : State p} {e : Expr (Tp.denote p) tp}
     constructor
     apply ih
     tauto
-  | callLambda h _ _ =>
-    intro hd
-    constructor <;> try tauto
-    simp_all
-    simp only [LawfulHeap.disjoint] at hd
-    simp only [Finmap.lookup_union_left (Finmap.mem_of_lookup_eq_some h)]
-    tauto
   | lam =>
     intros h
     simp only [LawfulHeap.disjoint, State.union_parts_left] at *
diff --git a/Lampe/Lampe/SeparationLogic/SLP.lean b/Lampe/Lampe/SeparationLogic/SLP.lean
index a0000f3..041f9c6 100644
--- a/Lampe/Lampe/SeparationLogic/SLP.lean
+++ b/Lampe/Lampe/SeparationLogic/SLP.lean
@@ -264,4 +264,11 @@ theorem wand_cancel [LawfulHeap α] {P Q : SLP α} : (P ⋆ (P -⋆ Q)) ⊢ Q :=
 
 end wand
 
+theorem extract_prop [LawfulHeap α] {H₁ H₂ : SLP α} (h₁ : (H₁ ⋆ H₂) st) (h₂ : H₁ ⊢ ⟦P⟧ ⋆ ⊤) : P := by
+  apply SLP.star_mono_r at h₂
+  apply SLP.ent_drop_left at h₁
+  apply h₂ at h₁
+  simp only [SLP.lift, SLP.top, SLP.star] at h₁
+  aesop
+
 end Lampe.SLP
diff --git a/Lampe/Lampe/Syntax.lean b/Lampe/Lampe/Syntax.lean
index 0ee115b..bd2f887 100644
--- a/Lampe/Lampe/Syntax.lean
+++ b/Lampe/Lampe/Syntax.lean
@@ -39,13 +39,17 @@ syntax nr_ident "<" nr_type,* ">" : nr_type -- Struct
 syntax "[" nr_type "]" : nr_type -- Slice
 syntax "[" nr_type ";" num "]" : nr_type -- Array
 syntax "`(" nr_type,* ")" : nr_type -- Tuple
+syntax "λ(" nr_type,* ")" "→" nr_type : nr_type -- Function
 
-def mkFieldName (structName : String) (fieldName : String) : Lean.Ident :=
+def mkFieldAccessorIdent (structName : String) (fieldName : String) : Lean.Ident :=
   mkIdent $ Name.mkSimple $ "field" ++ "#" ++ structName ++ "#" ++ fieldName
 
 def mkStructDefIdent (structName : String) : Lean.Ident :=
    mkIdent $ Name.mkSimple $ "struct" ++ "#" ++ structName
 
+def mkFunctionDefIdent (fnName : String) : Lean.Ident :=
+  mkIdent $ Name.mkSimple fnName
+
 def mkListLit [Monad m] [MonadQuotation m] [MonadExceptOf Exception m] [MonadError m] : List (TSyntax `term) → m (TSyntax `term)
 | [] => `([])
 | x :: xs => do
@@ -77,6 +81,10 @@ partial def mkNrType [Monad m] [MonadQuotation m] [MonadExceptOf Exception m] [M
 | `(nr_type| `($tps,* )) => do
   let tps ← tps.getElems.toList.mapM mkNrType
   `(Tp.tuple none $(←mkListLit tps))
+| `(nr_type| λ( $paramTps,* ) → $outTp) => do
+  let paramTps ← (mkListLit (←paramTps.getElems.toList.mapM mkNrType))
+  let outTp ← mkNrType outTp
+  `(Tp.fn $paramTps $outTp)
 | _ => throwUnsupportedSyntax
 
 def mkBuiltin [Monad m] [MonadQuotation m] [MonadExceptOf Exception m] [MonadError m] (i : String) : m (TSyntax `term) :=
@@ -93,7 +101,7 @@ def mkTupleMember [Monad m] [MonadQuotation m] [MonadExceptOf Exception m] [Mona
 
 def mkStructMember [Monad m] [MonadQuotation m] [MonadExceptOf Exception m] [MonadError m] (structName : TSyntax `nr_ident) (gs : List $ TSyntax `nr_type) (field : TSyntax `ident) : m (TSyntax `term) := do
   let gs ← mkHListLit (←gs.mapM fun gVal => mkNrType gVal)
-  let accessor := mkFieldName (←mkNrIdent structName) (field.getId.toString)
+  let accessor := mkFieldAccessorIdent (←mkNrIdent structName) (field.getId.toString)
   `($accessor $gs)
 
 syntax ident ":" nr_type : nr_param_decl
@@ -112,8 +120,6 @@ syntax "(" nr_expr ")" : nr_expr
 syntax "*(" nr_expr ")" : nr_expr
 syntax "|" nr_param_decl,* "|" "->" nr_type nr_expr : nr_expr
 
-syntax nr_typed_expr := nr_expr ":" nr_type
-
 syntax nr_ident "<" nr_type,* ">" "{" nr_expr,* "}" : nr_expr -- Struct constructor
 syntax "`(" nr_expr,* ")" : nr_expr -- Tuple constructor
 syntax "[" nr_expr,* "]" : nr_expr -- Array constructor
@@ -125,9 +131,11 @@ syntax nr_expr "[" nr_expr "]" : nr_expr -- Array access
 syntax nr_expr "[[" nr_expr "]]" : nr_expr -- Slice access
 
 syntax "#" nr_ident "(" nr_expr,* ")" ":" nr_type : nr_expr -- Builtin call
-syntax "(" nr_type "as" nr_ident "<" nr_type,* ">" ")" "::" nr_ident "<" nr_type,* ">" "(" nr_typed_expr,* ")" ":" nr_type : nr_expr -- Trait call
-syntax "^" nr_ident "(" nr_expr,* ")" ":" nr_type : nr_expr -- Lambda call
-syntax "@" nr_ident "<" nr_type,* ">" "(" nr_expr,* ")" ":" nr_type : nr_expr -- Decl call
+
+syntax "(" nr_type "as" nr_ident "<" nr_type,* ">" ")" "::" nr_ident "<" nr_type,* ">" "as" nr_type : nr_expr -- Trait func ident
+syntax "@" nr_ident "<" nr_type,* ">" "as" nr_type : nr_expr -- Decl func ident
+
+syntax nr_expr "(" nr_expr,* ")" : nr_expr -- Universal call
 
 syntax nr_fn_decl := nr_ident "<" ident,* ">" "(" nr_param_decl,* ")" "->" nr_type "{" sepBy(nr_expr, ";", ";", allowTrailingSep) "}"
 syntax nr_trait_constraint := nr_type ":" nr_ident "<" nr_type,* ">"
@@ -138,39 +146,39 @@ syntax nr_struct_def := "<" ident,* ">" "{" sepBy(nr_param_decl, ",", ",", allow
 
 @[reducible]
 def Expr.ref (val : rep tp) : Expr rep tp.ref :=
-  Expr.call h![] _ tp.ref (.builtin .ref) h![val]
+  Expr.callBuiltin _ tp.ref .ref h![val]
 
 @[reducible]
 def Expr.readRef (ref : rep tp.ref) : Expr rep tp :=
-  Expr.call h![] _ tp (.builtin .readRef) h![ref]
+  Expr.callBuiltin _ tp .readRef h![ref]
 
 @[reducible]
 def Expr.writeRef (ref : rep tp.ref) (val : rep tp) : Expr rep .unit :=
-  Expr.call h![] _ .unit (.builtin .writeRef) h![ref, val]
+  Expr.callBuiltin _ .unit .writeRef h![ref, val]
 
 @[reducible]
 def Expr.mkSlice (n : Nat) (vals : HList rep (List.replicate n tp)) : Expr rep (.slice tp) :=
-  Expr.call h![] _ (.slice tp) (.builtin $ .mkSlice n) vals
+  Expr.callBuiltin _ (.slice tp) (.mkSlice n) vals
 
 @[reducible]
 def Expr.mkArray (n : Nat) (vals : HList rep (List.replicate n tp)) : Expr rep (.array tp n) :=
-  Expr.call h![] _ (.array tp n) (.builtin $ .mkArray n) vals
+  Expr.callBuiltin _ (.array tp n) (.mkArray n) vals
 
 @[reducible]
 def Expr.mkTuple (name : Option String) (args : HList rep tps) : Expr rep (.tuple name tps) :=
-  Expr.call h![] tps (.tuple name tps) (.builtin .mkTuple) args
+  Expr.callBuiltin tps (.tuple name tps) ( .mkTuple) args
 
 @[reducible]
 def Expr.modifyLens (r : rep $ .ref tp₁) (v : rep tp₂) (lens : Lens rep tp₁ tp₂) : Expr rep .unit :=
-  Expr.call h![] [.ref tp₁, tp₂] .unit (.builtin $ .modifyLens lens) h![r, v]
+  Expr.callBuiltin [.ref tp₁, tp₂] .unit (.modifyLens lens) h![r, v]
 
 @[reducible]
 def Expr.readLens (r : rep $ .ref tp₁) (lens : Lens rep tp₁ tp₂) : Expr rep tp₂ :=
-  Expr.call h![] _ tp₂ (.builtin $ .readLens lens) h![r]
+  Expr.callBuiltin _ tp₂ (.readLens lens) h![r]
 
 @[reducible]
 def Expr.getLens (v : rep tp₁) (lens : Lens rep tp₁ tp₂) : Expr rep tp₂ :=
-  Expr.call h![] _ tp₂ (.builtin $ .getLens lens) h![v]
+  Expr.callBuiltin _ tp₂ (.getLens lens) h![v]
 
 structure DesugarState where
   autoDeref : Name → Bool
@@ -263,6 +271,13 @@ partial def getLeftmostExpr (expr : TSyntax `nr_expr) : (TSyntax `nr_expr) := ma
 | `(nr_expr| $sliceExpr:nr_expr [[ $_ ]]) => getLeftmostExpr sliceExpr
 | `(nr_expr| $e:nr_expr) => e
 
+partial def getFuncSignature [MonadSyntax m] (ty : TSyntax `nr_type) : m (List (TSyntax `term) × TSyntax `term) := match ty with
+| `(nr_type| λ( $paramTps,* ) → $outTp) => do
+  let paramTps ← paramTps.getElems.toList.mapM fun p => mkNrType p
+  let outTp ← mkNrType outTp
+  pure (paramTps, outTp)
+| _ => throwUnsupportedSyntax
+
 mutual
 
 partial def mkBlock [MonadSyntax m] (items: List (TSyntax `nr_expr)) (k : TSyntax `term → m (TSyntax `term)): m (TSyntax `term) := match items with
@@ -289,7 +304,7 @@ partial def mkArgs [MonadSyntax m] (args : List (TSyntax `nr_expr)) (k : List (T
     mkArgs t fun t => k (h :: t)
 
 partial def mkExpr [MonadSyntax m] (e : TSyntax `nr_expr) (vname : Option Lean.Ident) (k : TSyntax `term → m (TSyntax `term)): m (TSyntax `term) := match e with
-| `(nr_expr|$n:num : $tp) => do wrapSimple (←`(Expr.lit $(←mkNrType tp) $n)) vname k
+| `(nr_expr| $n:num : $tp) => do wrapSimple (←`(Expr.lit $(←mkNrType tp) $n)) vname k
 | `(nr_expr| true) => do wrapSimple (←`(Expr.lit Tp.bool 1)) vname k
 | `(nr_expr| false) => do wrapSimple (←`(Expr.lit Tp.bool 0)) vname k
 | `(nr_expr| { $exprs;* }) => mkBlock exprs.getElems.toList k
@@ -299,7 +314,7 @@ partial def mkExpr [MonadSyntax m] (e : TSyntax `nr_expr) (vname : Option Lean.I
   | some _ => wrapSimple (←`(Expr.var $i)) vname k
 | `(nr_expr| # $i:ident ($args,*): $tp) => do
   mkArgs args.getElems.toList fun argVals => do
-    wrapSimple (←`(Expr.call h![] _ $(←mkNrType tp) (.builtin $(←mkBuiltin i.getId.toString)) $(←mkHListLit argVals))) vname k
+    wrapSimple (←`(Expr.callBuiltin _ $(←mkNrType tp) $(←mkBuiltin i.getId.toString) $(←mkHListLit argVals))) vname k
 | `(nr_expr| for $i in $lo .. $hi $body) => do
   mkExpr lo none fun lo =>
   mkExpr hi none fun hi => do
@@ -340,27 +355,7 @@ partial def mkExpr [MonadSyntax m] (e : TSyntax `nr_expr) (vname : Option Lean.I
     | `(nr_param_decl|$i:ident : $_) => `($i)
     | _ => throwUnsupportedSyntax)
   let body ← mkExpr lambdaBody none fun x => `(Expr.var $x)
-  wrapSimple (←`(Expr.lambda $argTps $outTp (fun $args => $body))) vname k
-| `(nr_expr| ^ $i:ident ($args,*) : $tp) => do
-  mkArgs args.getElems.toList fun argVals => do
-    wrapSimple (←`(Expr.call h![] _ $(←mkNrType tp) (.lambda $i) $(←mkHListLit argVals))) vname k
-| `(nr_expr| @ $declName:nr_ident < $callGenVals:nr_type,* > ( $args,* ) : $tp) => do
-   let callGenKinds ← mkListLit (←callGenVals.getElems.toList.mapM fun _ => `(Kind.type))
-   let callGenVals ← mkHListLit (←callGenVals.getElems.toList.mapM fun gVal => mkNrType gVal)
-   mkArgs args.getElems.toList fun argVals => do
-     wrapSimple (←`(@Expr.call _ $callGenKinds $callGenVals _ $(←mkNrType tp) (.decl $(Syntax.mkStrLit (←mkNrIdent declName))) $(←mkHListLit argVals))) vname k
-| `(nr_expr| ( $selfTp as $traitName < $traitGenVals,* > ) :: $methodName < $callGenVals,* > ( $args,* ) : $tp) => do
-  let argTps ← args.getElems.toList.mapM fun arg => match arg with | `(nr_typed_expr| $_ : $ty) => mkNrType ty | _ => throwUnsupportedSyntax
-  let argExprs ← args.getElems.toList.mapM fun arg => match arg with | `(nr_typed_expr| $expr : $_) => pure expr | _ => throwUnsupportedSyntax
-  let callGenKinds ← mkListLit (←callGenVals.getElems.toList.mapM fun _ => `(Kind.type))
-  let callGenVals ← mkHListLit (←callGenVals.getElems.toList.mapM fun gVal => mkNrType gVal)
-  let traitGenKinds ← mkListLit (←traitGenVals.getElems.toList.mapM fun _ => `(Kind.type))
-  let traitGenVals ← mkHListLit (←traitGenVals.getElems.toList.mapM fun gVal => mkNrType gVal)
-  let methodName ← mkNrIdent methodName
-  let traitName ← mkNrIdent traitName
-  mkArgs argExprs fun argVals => do
-    wrapSimple (←`(@Expr.call _ $callGenKinds $callGenVals $(←mkListLit argTps) $(←mkNrType tp)
-      (.trait ⟨⟨⟨$(Syntax.mkStrLit traitName), $traitGenKinds, $traitGenVals⟩, $(←mkNrType selfTp)⟩, $(Syntax.mkStrLit methodName)⟩) $(←mkHListLit argVals))) vname k
+  wrapSimple (←`(Expr.lam $argTps $outTp (fun $args => $body))) vname k
 | `(nr_expr| $structName:nr_ident < $structGenVals,* > { $args,* }) => do
    let structName ← mkNrIdent structName
    let fieldTps ← `(Struct.fieldTypes $(mkStructDefIdent structName) $(←mkHListLit (←structGenVals.getElems.toList.mapM fun gVal => mkNrType gVal)))
@@ -369,6 +364,27 @@ partial def mkExpr [MonadSyntax m] (e : TSyntax `nr_expr) (vname : Option Lean.I
 | `(nr_expr| `( $args,* )) => do
   mkArgs args.getElems.toList fun argVals => do
     wrapSimple (←`(Expr.mkTuple none $(←mkHListLit argVals))) vname k
+| `(nr_expr| @ $fnName:nr_ident < $callGenVals:nr_type,* > as $t:nr_type) => do
+  let callGenKinds ← mkListLit (←callGenVals.getElems.toList.mapM fun _ => `(Kind.type))
+  let callGenVals ← mkHListLit (←callGenVals.getElems.toList.mapM fun gVal => mkNrType gVal)
+  let fnName := Syntax.mkStrLit (←mkNrIdent fnName)
+  let (paramTps, outTp) ← getFuncSignature t
+  wrapSimple (←`(Expr.fn $(←mkListLit paramTps) $outTp (FuncRef.decl $fnName $callGenKinds $callGenVals))) vname k
+| `(nr_expr| ( $selfTp as $traitName < $traitGenVals,* > ) :: $methodName < $callGenVals,* > as $t:nr_type) => do
+  let callGenKinds ← mkListLit (←callGenVals.getElems.toList.mapM fun _ => `(Kind.type))
+  let callGenVals ← mkHListLit (←callGenVals.getElems.toList.mapM fun gVal => mkNrType gVal)
+  let traitGenKinds ← mkListLit (←traitGenVals.getElems.toList.mapM fun _ => `(Kind.type))
+  let traitGenVals ← mkHListLit (←traitGenVals.getElems.toList.mapM fun gVal => mkNrType gVal)
+  let methodName := Syntax.mkStrLit (←mkNrIdent methodName)
+  let traitName := Syntax.mkStrLit (←mkNrIdent traitName)
+  let (paramTps, outTp) ← getFuncSignature t
+  wrapSimple (←`(Expr.fn $(←mkListLit paramTps) $outTp
+    (FuncRef.trait $(←mkNrType selfTp) $traitName $traitGenKinds $traitGenVals $methodName $callGenKinds $callGenVals))) vname k
+| `(nr_expr| $fnExpr:nr_expr ( $args:nr_expr,* )) => do
+  mkExpr fnExpr none fun fnRef => do
+    mkArgs args.getElems.toList fun argVals => do
+      let args ← mkHListLit argVals
+      wrapSimple (←`(Expr.call _ _ $fnRef $args)) vname k
 | `(nr_expr| ( $_:nr_expr as $_:nr_ident  < $_,* > ) . $_:ident)
 | `(nr_expr| $_:nr_expr . $_:num)
 | `(nr_expr| $_:nr_expr [ $_:nr_expr ])
@@ -451,7 +467,7 @@ def mkStructProjector [Monad m] [MonadQuotation m] [MonadExceptOf Exception m] [
         | $(←mkHListLit generics) => Builtin.Member $(←mkNrType paramType) (Struct.fieldTypes $(mkStructDefIdent (←mkNrIdent structName)) generics))
       let paramDefSyn ← `(match generics with
         | $(←mkHListLit generics) => $(←mkTupleMember idx))
-      let defnNameSyn := mkFieldName (←mkNrIdent structName) paramName.getId.toString
+      let defnNameSyn := mkFieldAccessorIdent (←mkNrIdent structName) paramName.getId.toString
       `(def $defnNameSyn (generics : HList Kind.denote $genericKinds) : $paramDefTy := $paramDefSyn)
     | _ => throwUnsupportedSyntax
 | _ => throwUnsupportedSyntax
@@ -466,7 +482,7 @@ elab "nrfn![" "fn" fn:nr_fn_decl "]" : term => do
 
 elab "nr_def" decl:nr_fn_decl : command => do
   let (name, decl) ← mkFnDecl decl
-  let decl ← `(def $(mkIdent $ Name.mkSimple name) : Lampe.FunctionDecl := $decl)
+  let decl ← `(def $(mkFunctionDefIdent name) : Lampe.FunctionDecl := $decl)
   Elab.Command.elabCommand decl
 
 elab "nr_trait_impl[" defName:ident "]" impl:nr_trait_impl : command => do
diff --git a/Lampe/Lampe/Tactic/SeparationLogic.lean b/Lampe/Lampe/Tactic/SeparationLogic.lean
index 0e15d3e..3be2229 100644
--- a/Lampe/Lampe/Tactic/SeparationLogic.lean
+++ b/Lampe/Lampe/Tactic/SeparationLogic.lean
@@ -209,11 +209,6 @@ def isLetIn (e : Expr) : Bool := e.isAppOf ``Lampe.Expr.letIn
 
 def isIte (e : Expr) : Bool := e.isAppOf `Lampe.Expr.ite
 
-def isCallTrait (e : Expr) : Bool := e.isAppOf `Lampe.Expr.call &&
-  match (e.getArg? 5) with
-  | some callTarget => callTarget.isAppOf `Lampe.FunctionIdent.trait
-  | _ => false
-
 partial def parseSLExpr (e: Expr): TacticM SLTerm := do
   if e.isAppOf ``SLP.star then
     let args := e.getAppArgs
@@ -384,19 +379,6 @@ theorem lmbSingleton_star_congr {p} {r} {v₁ v₂ : Lambda _} {R : SLP (State p
   rintro rfl
   apply SLP.entails_self
 
-lemma nested_triple {Q : _ → SLP (State p)}
-  (h_hoare_imp : STHoare p Γ P e₁ Q → STHoare p Γ (P ⋆ H) e₂ (fun v => Q v ⋆ H))
-  (h_hoare : STHoare p Γ P e₁ Q)
-  (h_ent_pre : H ⊢ P ⋆ H) :
-  STHoare p Γ H e₂ Q := by
-  have h_ent_post : ∀ v, ((Q v) ⋆ H) ⋆ ⊤ ⊢ (Q v) ⋆ ⊤ := by
-    simp [SLP.ent_drop_left]
-  have h_hoare' := h_hoare_imp h_hoare
-  apply consequence h_ent_pre (fun v => SLP.entails_self)
-  apply consequence SLP.entails_self h_ent_post
-  tauto
-
-
 def canSolveSingleton (lhs : SLTerm) (rhsV : Expr): Bool :=
   match lhs with
   | SLTerm.singleton v _ => v == rhsV
@@ -557,15 +539,12 @@ macro "stephelper1" : tactic => `(tactic|(
     | apply Lampe.STHoare.litField_intro
     | apply Lampe.STHoare.litTrue_intro
     | apply Lampe.STHoare.litFalse_intro
+    | apply fn_intro
     | apply fresh_intro
     | apply assert_intro
     | apply skip_intro
-    | apply nested_triple STHoare.callLambda_intro
     | apply lam_intro
     | apply cast_intro
-    | apply cast_intro
-    | apply callTrait_intro
-    | apply callDecl_intro
     -- memory
     | apply var_intro
     | apply ref_intro
@@ -631,6 +610,7 @@ macro "stephelper2" : tactic => `(tactic|(
     | apply consequence_frame_left Lampe.STHoare.litField_intro
     | apply consequence_frame_left Lampe.STHoare.litTrue_intro
     | apply consequence_frame_left Lampe.STHoare.litFalse_intro
+    | apply consequence_frame_left fn_intro
     | apply consequence_frame_left fresh_intro
     | apply consequence_frame_left assert_intro
     | apply consequence_frame_left lam_intro
@@ -701,12 +681,12 @@ macro "stephelper3" : tactic => `(tactic|(
     | apply ramified_frame_top Lampe.STHoare.litField_intro
     | apply ramified_frame_top Lampe.STHoare.litTrue_intro
     | apply ramified_frame_top Lampe.STHoare.litFalse_intro
+    | apply ramified_frame_top fn_intro
     | apply ramified_frame_top fresh_intro
     | apply ramified_frame_top assert_intro
     | apply ramified_frame_top skip_intro
     | apply ramified_frame_top lam_intro
     | apply ramified_frame_top cast_intro
-    | apply ramified_frame_top callDecl_intro
     -- memory
     | apply ramified_frame_top var_intro
     | apply ramified_frame_top ref_intro
diff --git a/Lampe/Lampe/Tp.lean b/Lampe/Lampe/Tp.lean
index 69d21fb..f9bf922 100644
--- a/Lampe/Lampe/Tp.lean
+++ b/Lampe/Lampe/Tp.lean
@@ -28,6 +28,19 @@ inductive Tp where
 | array (element: Tp) (size: U 32)
 | tuple (name : Option String) (fields : List Tp)
 | ref (tp : Tp)
+| fn (argTps : List Tp) (outTp : Tp)
+
+@[reducible]
+def Kind.denote : Kind → Type
+| .nat => Nat
+| .type => Tp
+
+inductive FuncRef (argTps : List Tp) (outTp : Tp) where
+| lambda (r : Ref)
+| decl (fnName : String) (kinds : List Kind) (generics : HList Kind.denote kinds)
+| trait (selfTp : Tp)
+  (traitName : String) (traitKinds : List Kind) (traitGenerics : HList Kind.denote traitKinds)
+  (fnName : String) (fnKinds : List Kind) (fnGenerics : HList Kind.denote fnKinds)
 
 mutual
 
@@ -49,13 +62,8 @@ def Tp.denote : Tp → Type
 | .array tp n => Mathlib.Vector (denote tp) n.toNat
 | .ref _ => Ref
 | .tuple _ fields => Tp.denoteArgs fields
+| .fn argTps outTp => FuncRef argTps outTp
 
 end
 
-@[reducible]
-def Kind.denote : Kind → Type
-| .nat => Nat
-| .type => Tp
-
-
 end Lampe