diff --git a/Strata/DL/Lambda/Factory.lean b/Strata/DL/Lambda/Factory.lean
index f86ae47d..c051852f 100644
--- a/Strata/DL/Lambda/Factory.lean
+++ b/Strata/DL/Lambda/Factory.lean
@@ -29,13 +29,16 @@ open Std (ToFormat Format format)
 
 open LTy.Syntax
 
-variable {Identifier : Type} [DecidableEq Identifier] [ToFormat Identifier] [Inhabited Identifier]
+variable {Identifier : Type} [DecidableEq Identifier] [ToFormat Identifier] [Inhabited Identifier] [Hashable Identifier]
 
 /--
 A signature is a map from variable identifiers to types.
 -/
 abbrev Signature (Identifier : Type) (Ty : Type) := Map Identifier Ty
 
+instance [Hashable Identifier] [Hashable Ty] : Hashable (Signature Identifier Ty) where
+  hash s := hash s
+
 def Signature.format (ty : Signature Identifier Ty) [Std.ToFormat Ty] : Std.Format :=
   match ty with
   | [] => ""
@@ -45,6 +48,9 @@ def Signature.format (ty : Signature Identifier Ty) [Std.ToFormat Ty] : Std.Form
 
 abbrev LMonoTySignature := Signature Identifier LMonoTy
 
+instance [Hashable Identifier] [Hashable LMonoTy]: Hashable (Signature Identifier LMonoTy) where
+  hash s := hash s
+
 abbrev LTySignature := Signature Identifier LTy
 
 
@@ -90,6 +96,12 @@ structure LFunc (Identifier : Type) where
   denote   : Option ((LExpr Identifier) → List (LExpr Identifier) → (LExpr Identifier)) := .none
   axioms   : List (LExpr Identifier) := []  -- For axiomatic definitions
 
+instance : Hashable (LFunc Identifier) where
+  hash f := hash (f.name, f.typeArgs, f.inputs, f.output, f.body, f.attr, f.axioms)
+
+instance : BEq (LFunc Identifier) where
+  beq a b := a.name == b.name && a.typeArgs == b.typeArgs && a.inputs == b.inputs && a.output == b.output && a.body == b.body && a.attr == b.attr && a.axioms == b.axioms
+
 instance : Inhabited (LFunc Identifier) where
   default := { name := Inhabited.default, inputs := [], output := LMonoTy.bool }
 
@@ -146,7 +158,14 @@ Identifier)` -- lambdas are our only tool. `Factory` gives us a way to add
 support for concrete/symbolic evaluation and type checking for `FunFactory`
 functions without actually modifying any core logic or the ASTs.
 -/
-def Factory := Array (LFunc Identifier)
+abbrev Factory := Array (LFunc Identifier)
+
+instance [Hashable Identifier] : Hashable (@Factory Identifier) where
+   hash a := hash (a : Array (LFunc Identifier))
+
+instance [BEq Identifier] : BEq (@Factory Identifier) where
+  beq a b := a == b
+
 
 def Factory.default : @Factory Identifier := #[]
 
diff --git a/Strata/DL/Lambda/LExpr.lean b/Strata/DL/Lambda/LExpr.lean
index 2c2cc9af..291f6538 100644
--- a/Strata/DL/Lambda/LExpr.lean
+++ b/Strata/DL/Lambda/LExpr.lean
@@ -22,7 +22,7 @@ open Std (ToFormat Format format)
 inductive QuantifierKind
   | all
   | exist
-  deriving Repr, DecidableEq
+  deriving Repr, DecidableEq, Hashable
 
 /--
 Lambda Expressions with Quantifiers.
@@ -57,7 +57,7 @@ inductive LExpr (Identifier : Type) : Type where
   | ite     (c t e : LExpr Identifier)
   /-- `.eq e1 e2`: equality expression. -/
   | eq      (e1 e2 : LExpr Identifier)
-  deriving Repr, DecidableEq
+  deriving Repr, DecidableEq, Hashable
 
 def LExpr.all {Identifier : Type} := @LExpr.quant Identifier .all
 def LExpr.exist {Identifier : Type} := @LExpr.quant Identifier .exist
diff --git a/Strata/DL/Lambda/LExprT.lean b/Strata/DL/Lambda/LExprT.lean
index 14284004..0bc47307 100644
--- a/Strata/DL/Lambda/LExprT.lean
+++ b/Strata/DL/Lambda/LExprT.lean
@@ -21,7 +21,7 @@ namespace Lambda
 open Std (ToFormat Format format)
 open LTy
 
-variable {Identifier : Type} [ToString Identifier] [DecidableEq Identifier] [ToFormat Identifier] [HasGen Identifier]
+variable {Identifier : Type} [ToString Identifier] [DecidableEq Identifier] [ToFormat Identifier] [HasGen Identifier] [Hashable Identifier]
 
 /--
 Monotype-annotated Lambda expressions, obtained after a type inference transform
@@ -38,7 +38,7 @@ inductive LExprT (Identifier : Type): Type where
   | app (fn e : LExprT Identifier) (ty : LMonoTy)
   | ite (c t e : LExprT Identifier) (ty : LMonoTy)
   | eq (e1 e2 : LExprT Identifier) (ty : LMonoTy)
-  deriving Repr, DecidableEq
+  deriving Repr, DecidableEq, Hashable
 
 partial def LExprT.format (et : (LExprT Identifier)) : Std.Format :=
   match et with
@@ -257,6 +257,7 @@ def inferConst (T : (TEnv Identifier)) (c : String) (cty : Option LMonoTy) :
       .error f!"Cannot infer the type of this constant: \
                 {@LExpr.const Identifier c cty}"
 
+
 mutual
 partial def fromLExprAux (T : (TEnv Identifier)) (e : (LExpr Identifier)) :
     Except Format ((LExprT Identifier) × (TEnv Identifier)) :=
@@ -406,11 +407,395 @@ partial def fromLExprAux.app (T : (TEnv Identifier)) (e1 e2 : (LExpr Identifier)
 
 end
 
+structure FromLExprAuxCache (Identifier: Type) [ToString Identifier] [DecidableEq Identifier] [ToFormat Identifier] [HasGen Identifier] [Hashable Identifier] where
+  cache : (Std.HashMap ((TEnv Identifier) × (LExpr Identifier)) (((LExprT Identifier) × (TEnv Identifier))))
+  valid : Prop :=
+    let hashMap := cache
+    ∀ (k : (TEnv Identifier) × (LExpr Identifier)) (v : ((LExprT Identifier) × (TEnv Identifier))),
+      hashMap.get? k = some v →
+        (match fromLExprAux k.1 k.2 with
+          | .ok vv => vv = v
+          | .error _ => false
+        )
+mutual
+partial def fromLExprAuxMem (cache : FromLExprAuxCache Identifier) (T : (TEnv Identifier)) (e : (LExpr Identifier)) :
+    Except Format ((LExprT Identifier) × (TEnv Identifier)) :=
+  open LTy.Syntax in do
+
+  let key := (T, e)
+
+  let hashMap := cache.cache
+  match hashMap.get? key with
+    | some result => return result
+    | none => do
+      let result ← match e with
+      | .mdata m e =>
+        let (et, T) ← fromLExprAuxMem cache T e
+        .ok ((.mdata m et), T)
+      | .const c cty =>
+        let (ty, T) ← inferConst T c cty
+        .ok (.const c ty, T)
+      | .op o oty =>
+        let (ty, T) ← inferOp T o oty
+        .ok (.op o ty, T)
+      | .bvar _ => .error f!"Cannot infer the type of this bvar: {e}"
+      | .fvar x fty =>
+        let (ty, T) ← inferFVar T x fty
+        .ok (.fvar x ty, T)
+      | .app e1 e2   => fromLExprAuxMem.app T e1 e2
+      | .abs ty e    => fromLExprAuxMem.abs T ty e
+      | .quant qk ty e => fromLExprAuxMem.quant T qk ty e
+      | .eq e1 e2    => fromLExprAuxMem.eq T e1 e2
+      | .ite c th el => fromLExprAuxMem.ite T c th el
+
+      -- Update cache
+      let currentMap := cache.cache
+      let newMap := (currentMap.insert key result)
+      let newCache: FromLExprAuxCache Identifier := {cache := newMap}
+      return result
+
+/-- Infer the type of an operation `.op o oty`, where an operation is defined in
+  the factory. -/
+partial def inferOpMem (T : (TEnv Identifier)) (o : Identifier) (oty : Option LMonoTy) :
+  Except Format (LMonoTy × (TEnv Identifier)) :=
+  open LTy.Syntax in
+  match T.functions.find? (fun fn => fn.name == o) with
+  | none =>
+    .error f!"{toString $ T.functions.getFunctionNames} Cannot infer the type of this operation: \
+              {LExpr.op (toString o) oty}"
+  | some func => do
+      -- `LFunc.type` below will also catch any ill-formed functions (e.g.,
+      -- where there are duplicates in the formals, etc.).
+      let type ← func.type
+      let (ty, T) ← LTy.instantiateWithCheck type T
+      let T ←
+        match func.body with
+        | none => .ok T
+        | some body =>
+          if body.freeVars.keys.all (fun k => k ∈ func.inputs.keys) then
+            -- Temporarily add formals in the context.
+            let T := T.pushEmptyContext
+            let T := T.addToContext func.inputPolyTypes
+            -- Type check the body and ensure that it unifies with the return type.
+            -- let (bodyty, T) ← infer T body
+            let (body_typed, T) ← fromLExprAuxMem T body
+            let bodyty := body_typed.toLMonoTy
+            let (retty, T) ← func.outputPolyType.instantiateWithCheck T
+            let S ← Constraints.unify [(retty, bodyty)] T.state.subst
+            let T := T.updateSubst S
+            let T := T.popContext
+            .ok T
+          else
+            .error f!"Function body contains free variables!\n\
+                      {func}"
+      match oty with
+      | none => .ok (ty, T)
+      | some cty =>
+        let S ← Constraints.unify [(cty, ty)] T.state.subst
+        .ok (ty, TEnv.updateSubst T S)
+
+partial def fromLExprAuxMem.ite (T : (TEnv Identifier)) (c th el : (LExpr Identifier)) := do
+  let (ct, T) ← fromLExprAuxMem T c
+  let (tt, T) ← fromLExprAuxMem T th
+  let (et, T) ← fromLExprAuxMem T el
+  let cty := ct.toLMonoTy
+  let tty := tt.toLMonoTy
+  let ety := et.toLMonoTy
+  let S ← Constraints.unify [(cty, LMonoTy.bool), (tty, ety)] T.state.subst
+  .ok (.ite ct tt et tty, TEnv.updateSubst T S)
+
+partial def fromLExprAuxMem.eq (T : (TEnv Identifier)) (e1 e2 : (LExpr Identifier)) := do
+  -- `.eq A B` is well-typed if there is some instantiation of
+  -- type parameters in `A` and `B` that makes them have the same type.
+  let (e1t, T) ← fromLExprAux T e1
+  let (e2t, T) ← fromLExprAux T e2
+  let ty1 := e1t.toLMonoTy
+  let ty2 := e2t.toLMonoTy
+  let S ← Constraints.unify [(ty1, ty2)] T.state.subst
+  .ok (.eq e1t e2t LMonoTy.bool, TEnv.updateSubst T S)
+
+partial def fromLExprAuxMem.abs (T : (TEnv Identifier)) (oty : Option LMonoTy) (e : (LExpr Identifier)) := do
+  let (xv, T) := HasGen.genVar T
+  let (xt', T) := TEnv.genTyVar T
+  let xt := .forAll [] (.ftvar xt')
+  let T := T.insertInContext xv xt
+  let e' := LExpr.varOpen 0 (xv, some (.ftvar xt')) e
+  let (et, T) ← fromLExprAuxMem T e'
+  let ety := et.toLMonoTy
+  let etclosed := .varClose 0 xv et
+  let T := T.eraseFromContext xv
+  let ty := (.tcons "arrow" [(.ftvar xt'), ety])
+  let mty := LMonoTy.subst T.state.subst ty
+  match mty, oty with
+  | .arrow aty _, .some ty =>
+    if aty == ty
+    then .ok ()
+    else .error "Type annotation on LTerm.abs doesn't match inferred argument type"
+  | _, _ => .ok ()
+  .ok (.abs etclosed mty, T)
+
+partial def fromLExprAuxMem.quant (T : (TEnv Identifier)) (qk : QuantifierKind) (oty : Option LMonoTy) (e : (LExpr Identifier)) := do
+  let (xv, T) := HasGen.genVar T
+  let (xt', T) := TEnv.genTyVar T
+  let xt := .forAll [] (.ftvar xt')
+  let S ← match oty with
+  | .some ty =>
+    let (optTyy, T) := (ty.aliasInst T)
+    (Constraints.unify [(.ftvar xt', optTyy.getD ty)] T.state.subst)
+  | .none =>
+    .ok T.state.subst
+
+  let T := TEnv.updateSubst T S
+
+  let T := T.insertInContext xv xt
+  let e' := LExpr.varOpen 0 (xv, some (.ftvar xt')) e
+  let (et, T) ← fromLExprAuxMem T e'
+  let ety := et.toLMonoTy
+  let mty := LMonoTy.subst T.state.subst (.ftvar xt')
+  match oty with
+  | .some ty =>
+    let (optTyy, _) := (ty.aliasInst T)
+    if optTyy.getD ty == mty
+    then .ok ()
+    else .error f!"Type annotation on LTerm.quant {ty} (alias for {optTyy.getD ty}) doesn't match inferred argument type"
+  | _ => .ok ()
+  if ety = LMonoTy.bool then do
+    let etclosed := .varClose 0 xv et
+    let T := T.eraseFromContext xv
+    .ok (.quant qk mty etclosed, T)
+  else
+    .error f!"Quantifier body has non-Boolean type: {ety}"
+
+partial def fromLExprAuxMem.app (T : (TEnv Identifier)) (e1 e2 : (LExpr Identifier)) := do
+  let (e1t, T) ← fromLExprAuxMem T e1
+  let ty1 := e1t.toLMonoTy
+  let (e2t, T) ← fromLExprAuxMem T e2
+  let ty2 := e2t.toLMonoTy
+  let (fresh_name, T) := TEnv.genTyVar T
+  let freshty := (.ftvar fresh_name)
+  let S ← Constraints.unify [(ty1, (.tcons "arrow" [ty2, freshty]))] T.state.subst
+  let mty := LMonoTy.subst S freshty
+  .ok (.app e1t e2t mty, TEnv.updateSubst T S)
+
+end
+-- mutual
+-- partial def fromLExprAuxMem (cache : FromLExprAuxCache Identifier) (T : (TEnv Identifier)) (e : (LExpr Identifier)) :
+--     IO (Except Format ((LExprT Identifier) × (TEnv Identifier))) :=
+--   open LTy.Syntax in do
+--   let key := (T, e)
+
+--   -- Check cache first
+--   let hashMap ← cache.cache.get
+--   match hashMap.get? key with
+--   | some result => return result
+--   | none => do
+--     -- Compute result
+--     let result ← match e with
+--       | .mdata m e => do
+--         let etResult ← fromLExprAuxMem cache T e
+--         match etResult with
+--         | .error err => return .error err
+--         | .ok (et, T) => return .ok ((.mdata m et), T)
+--       | .const c cty => do
+--         let tyResult := inferConst T c cty
+--         match tyResult with
+--         | .error err => return .error err
+--         | .ok (ty, T) => return .ok (.const c ty, T)
+--       | .op o oty => do
+--         let tyResult := inferOpMem cache T o oty
+--         match tyResult with
+--         | .error err => return .error err
+--         | .ok (ty, T) => return .ok (.op o ty, T)
+--       | .bvar _ => return .error f!"Cannot infer the type of this bvar: {e}"
+--       | .fvar x fty => do
+--         let tyResult := inferFVar T x fty
+--         match tyResult with
+--         | .error err => return .error err
+--         | .ok (ty, T) => return .ok (.fvar x ty, T)
+--       | .app e1 e2   => fromLExprAuxMem.app cache T e1 e2
+--       | .abs ty e    => fromLExprAuxMem.abs cache T ty e
+--       | .quant qk ty e => fromLExprAuxMem.quant cache T qk ty e
+--       | .eq e1 e2    => fromLExprAuxMem.eq cache T e1 e2
+--       | .ite c th el => fromLExprAuxMem.ite cache T c th el
+
+--     -- Update cache
+--     let currentMap ← cache.cache.get
+--     let newMap := currentMap.insert key result
+--     cache.cache.set newMap
+--     return result
+
+-- partial def inferOpMem (cache : FromLExprAuxCache Identifier) (T : (TEnv Identifier)) (o : Identifier) (oty : Option LMonoTy) :
+--   IO (Except Format (LMonoTy × (TEnv Identifier))) := do
+--   open LTy.Syntax in
+--   match T.functions.find? (fun fn => fn.name == o) with
+--   | none =>
+--     return .error f!"{toString $ T.functions.getFunctionNames} Cannot infer the type of this operation: \
+--               {LExpr.op (toString o) oty}"
+--   | some func => do
+--       let typeResult := func.type
+--       match typeResult with
+--       | .error err => return .error err
+--       | .ok type => do
+--         let tyResult := LTy.instantiateWithCheck type T
+--         match tyResult with
+--         | .error err => return .error err
+--         | .ok (ty, T) => do
+--           let TResult ←
+--             match func.body with
+--             | none => return .ok T
+--             | some body =>
+--               if body.freeVars.keys.all (fun k => k ∈ func.inputs.keys) then
+--                 let T := T.pushEmptyContext
+--                 let T := T.addToContext func.inputPolyTypes
+--                 let bodyResult ← fromLExprAuxMem cache T body
+--                 match bodyResult with
+--                 | .error err => return .error err
+--                 | .ok (body_typed, T) => do
+--                   let bodyty := body_typed.toLMonoTy
+--                   let rettyResult := func.outputPolyType.instantiateWithCheck T
+--                   match rettyResult with
+--                   | .error err => return .error err
+--                   | .ok (retty, T) => do
+--                     let SResult := Constraints.unify [(retty, bodyty)] T.state.subst
+--                     match SResult with
+--                     | .error err => return .error err
+--                     | .ok S => do
+--                       let T := T.updateSubst S
+--                       let T := T.popContext
+--                       return .ok T
+--               else
+--                 return .error f!"Function body contains free variables!\n\
+--                           {func}"
+--           match TResult with
+--           | .error err => return .error err
+--           | .ok T => do
+--             match oty with
+--             | none => return .ok (ty, T)
+--             | some cty =>
+--               let SResult := Constraints.unify [(cty, ty)] T.state.subst
+--               match SResult with
+--               | .error err => return .error err
+--               | .ok S => return .ok (ty, TEnv.updateSubst T S)
+
+-- partial def fromLExprAuxMem.ite (cache : FromLExprAuxCache Identifier) (T : (TEnv Identifier)) (c th el : (LExpr Identifier)) : IO (Except Format ((LExprT Identifier) × (TEnv Identifier))) := do
+--   let ctResult ← fromLExprAuxMem cache T c
+--   match ctResult with
+--   | .error err => return .error err
+--   | .ok (ct, T) => do
+--     let ttResult ← fromLExprAuxMem cache T th
+--     match ttResult with
+--     | .error err => return .error err
+--     | .ok (tt, T) => do
+--       let etResult ← fromLExprAuxMem cache T el
+--       match etResult with
+--       | .error err => return .error err
+--       | .ok (et, T) => do
+--         let tty := tt.toLMonoTy
+--         let ety := et.toLMonoTy
+--         let SResult := Constraints.unify [(tty, ety)] T.state.subst
+--         match SResult with
+--         | .error err => return .error err
+--         | .ok S => return .ok (.ite ct tt et tty, TEnv.updateSubst T S)
+
+-- partial def fromLExprAuxMem.eq (cache : FromLExprAuxCache Identifier) (T : (TEnv Identifier)) (e1 e2 : (LExpr Identifier)) : IO (Except Format ((LExprT Identifier) × (TEnv Identifier))) := do
+--   let e1Result ← fromLExprAuxMem cache T e1
+--   match e1Result with
+--   | .error err => return .error err
+--   | .ok (e1t, T) => do
+--     let e2Result ← fromLExprAuxMem cache T e2
+--     match e2Result with
+--     | .error err => return .error err
+--     | .ok (e2t, T) => do
+--       let e1ty := e1t.toLMonoTy
+--       let e2ty := e2t.toLMonoTy
+--       let SResult := Constraints.unify [(e1ty, e2ty)] T.state.subst
+--       match SResult with
+--       | .error err => return .error err
+--       | .ok S => return .ok (.eq e1t e2t LMonoTy.bool, TEnv.updateSubst T S)
+
+-- partial def fromLExprAuxMem.abs (cache : FromLExprAuxCache Identifier) (T : (TEnv Identifier)) (oty : Option LMonoTy) (e : (LExpr Identifier)) : IO (Except Format ((LExprT Identifier) × (TEnv Identifier))) := do
+--   let (xv, T) := HasGen.genVar T
+--   let (xt', T) := TEnv.genTyVar T
+--   let xt := .ftvar xt'
+--   let T := T.insertInContext xv (.forAll [] xt)
+--   let eopen := e.varOpen 0 (.fvar xv none)
+--   let etResult ← fromLExprAuxMem cache T eopen
+--   match etResult with
+--   | .error err => return .error err
+--   | .ok (et, T) => do
+--     let ety := et.toLMonoTy
+--     let mty := .arrow xt ety
+--     let T := T.eraseFromContext xv
+--     let etclosed := et.varClose 0 xv
+--     match oty with
+--     | none => return .ok (.abs etclosed mty, T)
+--     | some aty => do
+--       let SResult := Constraints.unify [(aty, mty)] T.state.subst
+--       match SResult with
+--       | .error err => return .error err
+--       | .ok S => return .ok (.abs etclosed mty, T)
+
+-- partial def fromLExprAuxMem.quant (cache : FromLExprAuxCache Identifier) (T : (TEnv Identifier)) (qk : QuantifierKind) (oty : Option LMonoTy) (e : (LExpr Identifier)) : IO (Except Format ((LExprT Identifier) × (TEnv Identifier))) := do
+--   let (xv, T) := HasGen.genVar T
+--   let (xt', T) := TEnv.genTyVar T
+--   let xt := .ftvar xt'
+--   let T := T.insertInContext xv (.forAll [] xt)
+--   let eopen := e.varOpen 0 (.fvar xv none)
+--   let etResult ← fromLExprAuxMem cache T eopen
+--   match etResult with
+--   | .error err => return .error err
+--   | .ok (et, T) => do
+--     let ety := et.toLMonoTy
+--     let T := T.eraseFromContext xv
+--     let etclosed := et.varClose 0 xv
+--     match oty with
+--     | none =>
+--       if ety == LMonoTy.bool then
+--         return .ok (.quant qk etclosed LMonoTy.bool, T)
+--       else
+--         return .error f!"Quantifier body has non-Boolean type: {ety}"
+--     | some aty => do
+--       let SResult := Constraints.unify [(aty, LMonoTy.bool)] T.state.subst
+--       match SResult with
+--       | .error err => return .error err
+--       | .ok S => do
+--         let T := TEnv.updateSubst T S
+--         if ety == LMonoTy.bool then
+--           return .ok (.quant qk etclosed LMonoTy.bool, T)
+--         else
+--           return .error f!"Quantifier body has non-Boolean type: {ety}"
+
+-- partial def fromLExprAuxMem.app (cache : FromLExprAuxCache Identifier) (T : (TEnv Identifier)) (e1 e2 : (LExpr Identifier)) : IO (Except Format ((LExprT Identifier) × (TEnv Identifier))) := do
+--   let e1Result ← fromLExprAuxMem cache T e1
+--   match e1Result with
+--   | .error err => return .error err
+--   | .ok (e1t, T) => do
+--     let ty1 := e1t.toLMonoTy
+--     let e2Result ← fromLExprAuxMem cache T e2
+--     match e2Result with
+--     | .error err => return .error err
+--     | .ok (e2t, T) => do
+--       let ty2 := e2t.toLMonoTy
+--       let (retty', T) := TEnv.genTyVar T
+--       let retty := .ftvar retty'
+--       let SResult := Constraints.unify [(ty1, .arrow ty2 retty)] T.state.subst
+--       match SResult with
+--       | .error err => return .error err
+--       | .ok S => return .ok (.app e1t e2t retty, TEnv.updateSubst T S)
+-- end
+
 protected def fromLExpr (T : (TEnv Identifier)) (e : (LExpr Identifier)) :
     Except Format ((LExprT Identifier) × (TEnv Identifier)) := do
   let (et, T) ← fromLExprAux T e
   .ok (LExprT.applySubst et T.state.subst, T)
 
+protected def fromLExprMem (cache : FromLExprAuxCache Identifier) (T : (TEnv Identifier)) (e : (LExpr Identifier)) :
+    IO (Except Format ((LExprT Identifier) × (TEnv Identifier))) := do
+  let etResult ← fromLExprAuxMem cache T e
+  match etResult with
+  | .error err => return .error err
+  | .ok (et, T) => return .ok (LExprT.applySubst et T.state.subst, T)
+
 protected def fromLExprs (T : (TEnv Identifier)) (es : List (LExpr Identifier)) :
     Except Format (List (LExprT Identifier) × (TEnv Identifier)) := do
   match es with
diff --git a/Strata/DL/Lambda/LExprTypeEnv.lean b/Strata/DL/Lambda/LExprTypeEnv.lean
index ec29a735..49070e38 100644
--- a/Strata/DL/Lambda/LExprTypeEnv.lean
+++ b/Strata/DL/Lambda/LExprTypeEnv.lean
@@ -27,7 +27,7 @@ structure TypeAlias where
   args : List TyIdentifier
   lhs  : LMonoTy
   rhs  : LMonoTy
-  deriving DecidableEq, Repr
+  deriving DecidableEq, Repr, Hashable
 
 instance : ToFormat TypeAlias where
   format a :=
@@ -49,7 +49,7 @@ cycles in the map.
 structure TContext (Identifier : Type) where
   types   :  Maps Identifier LTy := []
   aliases :  List TypeAlias := []
-  deriving DecidableEq, Repr
+  deriving DecidableEq, Repr, Hashable, BEq
 
 instance : ToFormat (TContext Identifier) where
   format ctx :=
@@ -148,7 +148,7 @@ structure TState where
   exprGen : Nat := 0
   exprPrefix : String := "$__var"
   subst : Subst := []
-  deriving DecidableEq, Repr
+  deriving DecidableEq, Repr, Hashable
 
 def TState.init : TState := {}
 
@@ -183,6 +183,11 @@ instance : ToFormat TState where
 /-- Track registered types. -/
 abbrev KnownTypes := List LTy
 
+instance:  Hashable KnownTypes where
+  hash kt := match kt with
+    | [] => hash kt
+    | hd :: tl => hash (hash (hd), (hash tl))
+
 /--
 A type environment `TEnv` contains a stack of contexts `TContext` to track `LExpr`
 variables and their types, a typing state `TState` to track the global
@@ -195,6 +200,10 @@ structure TEnv (Identifier : Type) where
   state : TState
   functions : @Factory Identifier
   knownTypes : KnownTypes
+deriving Hashable
+
+instance : BEq (TEnv Identifier) where
+  beq a b := a.context == b.context && a.state == b.state && a.functions == b.functions && a.knownTypes == b.knownTypes
 
 def TEnv.default : TEnv Identifier :=
   open LTy.Syntax in
diff --git a/Strata/DL/Lambda/LTy.lean b/Strata/DL/Lambda/LTy.lean
index 9fc6d73d..3fcb1af6 100644
--- a/Strata/DL/Lambda/LTy.lean
+++ b/Strata/DL/Lambda/LTy.lean
@@ -33,7 +33,7 @@ inductive LMonoTy : Type where
   -- Type constructor.
   | tcons (name : String) (args : List LMonoTy)
   | bitvec (size : Nat)
-  deriving Inhabited, Repr
+  deriving Inhabited, Repr, Hashable
 
 abbrev LMonoTys := List LMonoTy
 
@@ -108,7 +108,7 @@ Type schemes (poly-types) in Lambda.
 -/
 inductive LTy : Type where
   | forAll (vars : List TyIdentifier) (ty : LMonoTy)
-  deriving Inhabited, Repr
+  deriving Inhabited, Repr, Hashable
 
 abbrev LTys := List LTy
 
diff --git a/Strata/DL/Lambda/LTyUnify.lean b/Strata/DL/Lambda/LTyUnify.lean
index 1aaaf1b4..05504a0c 100644
--- a/Strata/DL/Lambda/LTyUnify.lean
+++ b/Strata/DL/Lambda/LTyUnify.lean
@@ -25,6 +25,13 @@ open Std (ToFormat Format format)
 /-- Substitution mapping type variables to `LMonoTy`. -/
 abbrev Subst := Map TyIdentifier LMonoTy
 
+instance : Hashable (Subst) where
+  hash m := match m with
+    | [] => 0
+    | (k,v) :: rest => mixHash (mixHash (hash k) (hash v)) (hash rest)
+
+
+
 private def formatSubst (S : Subst) : Format :=
   match S with
   | [] => ""
diff --git a/Strata/DL/Lambda/MetaData.lean b/Strata/DL/Lambda/MetaData.lean
index abd6eebb..f57c7fc2 100644
--- a/Strata/DL/Lambda/MetaData.lean
+++ b/Strata/DL/Lambda/MetaData.lean
@@ -13,6 +13,6 @@ modify along with our code transformation functions.
 -/
 structure Info where
   value : String
-  deriving DecidableEq, Repr
+  deriving DecidableEq, Repr, Hashable
 
 end Lambda
diff --git a/Strata/DL/Util/Map.lean b/Strata/DL/Util/Map.lean
index 49e630fa..ba8d1c63 100644
--- a/Strata/DL/Util/Map.lean
+++ b/Strata/DL/Util/Map.lean
@@ -17,6 +17,12 @@ A simple Map-like type based on lists
 
 abbrev Map (α : Type u) (β : Type v) := List (α × β)
 
+instance [Hashable α] [Hashable β] : Hashable (Map α β) where
+  hash m := match m with
+    | [] => 0
+    | (k,v) :: rest => mixHash (mixHash (hash k) (hash v)) (hash rest)
+
+
 instance [BEq α] [BEq β] : BEq (Map α β) where
   beq m1 m2 := go m1 m2 where
   go m1 m2 :=