diff --git a/SciLean.lean b/SciLean.lean
index e70ca6e0..bc840585 100644
--- a/SciLean.lean
+++ b/SciLean.lean
@@ -12,6 +12,7 @@ import SciLean.Tactic.FTrans.Basic
 import SciLean.Tactic.FProp.Notation
 import SciLean.FTrans.FDeriv.Basic
 import SciLean.FunctionSpaces.Differentiable.Basic
+import SciLean.FTrans.CDeriv.Basic
 
 /-!
 
diff --git a/SciLean/FTrans/FDeriv/Basic.lean b/SciLean/FTrans/FDeriv/Basic.lean
index 8e6b8fa6..57839d31 100644
--- a/SciLean/FTrans/FDeriv/Basic.lean
+++ b/SciLean/FTrans/FDeriv/Basic.lean
@@ -10,7 +10,7 @@ import Mathlib.Analysis.Calculus.Deriv.Basic
 import Mathlib.Analysis.Calculus.Deriv.Inv 
 
 
-import SciLean.FunctionSpaces.ContinuousLinearMap.Basic
+import SciLean.FunctionSpaces.ContinuousLinearMap.Notation
 import SciLean.FunctionSpaces.Differentiable.Basic
 import SciLean.Tactic.FTrans.Basic
 
@@ -35,11 +35,43 @@ theorem fderiv.id_rule
   : (fderiv K fun x : X => x) = fun _ => fun dx =>L[K] dx
   := by ext x dx; simp
 
-
 theorem fderiv.const_rule (x : X)
   : (fderiv K fun _ : Y => x) = fun _ => fun dx =>L[K] 0
   := by ext x dx; simp
 
+theorem fderiv.comp_rule_at
+  (x : X)
+  (g : X → Y) (hg : DifferentiableAt K g x)
+  (f : Y → Z) (hf : DifferentiableAt K f (g x))
+  : (fderiv K fun x : X => f (g x)) x
+    =
+    let y := g x
+    fun dx =>L[K]
+      let dy := fderiv K g x dx
+      let dz := fderiv K f y dy
+      dz :=
+by 
+  rw[show (fun x => f (g x)) = f ∘ g by rfl]
+  rw[fderiv.comp x hf hg]
+  ext dx; simp
+
+theorem fderiv.comp_rule
+  (g : X → Y) (hg : Differentiable K g)
+  (f : Y → Z) (hf : Differentiable K f)
+  : (fderiv K fun x : X => f (g x))
+    =
+    fun x => 
+      let y := g x
+      fun dx =>L[K]
+        let dy := fderiv K g x dx
+        let dz := fderiv K f y dy
+        dz :=
+by 
+  funext x;
+  rw[show (fun x => f (g x)) = f ∘ g by rfl]
+  rw[fderiv.comp x (hf (g x)) (hg x)]
+  ext dx; simp
+
 
 theorem fderiv.let_rule_at
   (x : X)
@@ -54,12 +86,14 @@ theorem fderiv.let_rule_at
     fun dx =>L[K]
       let dy := fderiv K g x dx
       let dz := fderiv K (fun xy : X×Y => f xy.1 xy.2) (x,y) (dx, dy)
-      dz := 
-by 
+      dz :=
+by
   have h : (fun x => f x (g x)) = (fun xy : X×Y => f xy.1 xy.2) ∘ (fun x => (x, g x)) := by rfl
-  rw[h]
-  rw[fderiv.comp x hf (DifferentiableAt.prod (by simp) hg)]
-  rw[DifferentiableAt.fderiv_prod (by simp) hg]
+  conv => 
+    lhs
+    rw[h]
+    rw[fderiv.comp x hf (DifferentiableAt.prod (by simp) hg)]
+    rw[DifferentiableAt.fderiv_prod (by simp) hg]
   ext dx; simp[ContinuousLinearMap.comp]
   rfl
 
@@ -107,12 +141,19 @@ theorem fderiv.pi_rule
 
 open Lean Meta Qq
 
-def fderiv.discharger (e : Expr) : SimpM (Option Expr) :=
-  FTrans.tacticToDischarge (Syntax.mkLit ``tacticDifferentiable "differentiable") e
+def fderiv.discharger (e : Expr) : SimpM (Option Expr) := do
+  withTraceNode `fderiv_discharger (fun _ => return s!"discharge {← ppExpr e}") do
+  let cache := (← get).cache
+  let config : FProp.Config := {}
+  let state  : FProp.State := { cache := cache }
+  let (proof?, state) ← FProp.fprop e |>.run config |>.run state
+  modify (fun simpState => { simpState with cache := state.cache })
+  return proof?
 
 open Lean Elab Term FTrans
 def fderiv.ftransExt : FTransExt where
   ftransName := ``fderiv
+
   getFTransFun? e := 
     if e.isAppOf ``fderiv then
 
@@ -131,6 +172,7 @@ def fderiv.ftransExt : FTransExt where
 
   identityRule     := .some <| .thm ``fderiv.id_rule
   constantRule     := .some <| .thm ``fderiv.const_rule
+  compRule         := .some <| .thm ``fderiv.comp_rule
   lambdaLetRule    := .some <| .thm ``fderiv.let_rule
   lambdaLambdaRule := .some <| .thm ``fderiv.pi_rule
 
diff --git a/SciLean/FTrans/FDeriv/Test.lean b/SciLean/FTrans/FDeriv/Test.lean
index 11528ea1..a412df5e 100644
--- a/SciLean/FTrans/FDeriv/Test.lean
+++ b/SciLean/FTrans/FDeriv/Test.lean
@@ -3,6 +3,9 @@ import SciLean.Profile
 
 open SciLean
 
+-- #profile_this_file
+
+set_option profiler true
 
 variable {K : Type _} [NontriviallyNormedField K]
 
@@ -14,24 +17,23 @@ variable {ι : Type _} [Fintype ι]
 
 variable {E : ι → Type _} [∀ i, NormedAddCommGroup (E i)] [∀ i, NormedSpace K (E i)]
 
-example : NormedCommRing K := by infer_instance
-example : NormedAlgebra K K := by infer_instance
-
-example 
-  : fderiv K (fun (x : K) => x * x * x)
-    =
-    fun x => fun dx =>L[K] dx * x + dx * x  := 
-by 
-  ftrans only
-  set_option trace.Meta.Tactic.simp.rewrite true in
-  set_option trace.Meta.Tactic.simp.discharge true in
-  set_option trace.Meta.Tactic.simp.unify true in
-  set_option trace.Meta.Tactic.lsimp.pre true in
-  set_option trace.Meta.Tactic.lsimp.step true in
-  set_option trace.Meta.Tactic.lsimp.post true in
-  ftrans only
-  ext x; simp
+#exits
+-- example 
+--   : fderiv K (fun (x : K) => x * x * x)
+--     =
+--     fun x => fun dx =>L[K] dx * x + dx * x  := 
+-- by 
+--   ftrans only
+--   set_option trace.Meta.Tactic.simp.rewrite true in
+--   set_option trace.Meta.Tactic.simp.discharge true in
+--   set_option trace.Meta.Tactic.simp.unify true in
+--   set_option trace.Meta.Tactic.lsimp.pre true in
+--   set_option trace.Meta.Tactic.lsimp.step true in
+--   set_option trace.Meta.Tactic.lsimp.post true in
+--   ftrans only
+--   ext x; simp
 
+example : Differentiable K fun x : K => x := by fprop
 
 example 
   : fderiv K (fun (x : K) => x + x)
@@ -42,30 +44,59 @@ by
   ftrans only
   ext x; simp
 
-
 example 
   : fderiv K (fun (x : K) => x + x + x)
     =
     fun x => fun dx =>L[K]
       dx + dx + dx := 
 by 
-  ftrans only
+  ftrans only;
   ext x; simp
 
+example 
+  : fderiv K (fun (x : K) => x * x * x * x)
+    =
+    fun x => fun dx =>L[K] 0 := 
+by
+  conv =>
+    lhs
+    ftrans only
+  sorry
+
+
+set_option trace.Meta.Tactic.simp.rewrite true in
 example 
   : fderiv K (fun (x : K) => x + x + x + x)
     =
     fun x => fun dx =>L[K]
       dx + dx + dx + dx := 
 by 
-  ftrans only
-  ext x; simp
+  ftrans
 
-example 
-  : fderiv K (fun (x : K) => x + x + x + x + x)
+
+variable {K : Type _} [NontriviallyNormedField K]
+
+variable {E : Type _} [NormedAddCommGroup E] [NormedSpace K E]
+
+variable {F : Type _} [NormedAddCommGroup F] [NormedSpace K F]
+
+variable {G : Type _} [NormedAddCommGroup G] [NormedSpace K G]
+
+variable {f f₀ f₁ g : E → F}
+
+theorem fderiv_add' 
+  (hf : Differentiable K f) (hg : Differentiable K g) :
+    fderiv K (fun y => f y + g y) 
+    = 
+    fun x =>
+    fun dx =>L[K] 
+      fderiv K f x dx + fderiv K g x dx := sorry
+
+example (x : K)
+  : fderiv K (fun (x : K) => x + x + x + x + x) x
     =
-    fun x => fun dx =>L[K]
+    fun dx =>L[K]
       dx + dx + dx + dx + dx := 
-by 
-  ftrans only
-  ext x; simp
+by
+  simp (discharger:=fprop) only [fderiv_add', fderiv_id']
+  dsimp
diff --git a/SciLean/FTrans/FwdDeriv/Basic.lean b/SciLean/FTrans/FwdDeriv/Basic.lean
new file mode 100644
index 00000000..e8534d2a
--- /dev/null
+++ b/SciLean/FTrans/FwdDeriv/Basic.lean
@@ -0,0 +1,244 @@
+import SciLean.FTrans.FDeriv.Basic
+import SciLean.Profile
+
+namespace SciLean
+
+/-- `BroadcastType tag X ι MX` says that `MX` is `ι`-many copies of `X`
+
+  `tag` is used to indicate the class of broadcasting types. For example, dense or sparse matrices are broadcast type for vectors.
+  -/
+class BroadcastType (tag : Name) (R : Type _) [Ring R] (ι : Type _) (X : Type _) (MX : outParam $ Type _) [AddCommGroup X] [Module R X] [AddCommGroup MX] [Module R MX] where
+  equiv  : MX ≃ₗ[R] (ι → X)
+
+
+
+
+variable 
+  {R : Type _} [Ring R]
+  {X : Type _} [AddCommGroup X] [Module R X]
+  {Y : Type _} [AddCommGroup Y] [Module R Y]
+  {MX : Type _} [AddCommGroup MX] [Module R MX]
+  {MY : Type _} [AddCommGroup MY] [Module R MY]
+  {ι : Type _} -- [Fintype ι]
+  {κ : Type _} -- [Fintype κ]
+  {E ME : κ → Type _} 
+  [∀ j, AddCommGroup (E j)] [∀ j, Module R (E j)]
+  [∀ j, AddCommGroup (ME j)] [∀ j, Module R (ME j)]
+
+
+def broadcast (tag : Name) [BroadcastType tag R ι X MX] [BroadcastType tag R ι Y MY] 
+ (f : X → Y) : MX → MY := fun mx =>
+  (BroadcastType.equiv tag (R:=R)).invFun fun (i : ι) => f ((BroadcastType.equiv tag (R:=R)) mx i)
+
+ 
+open BroadcastType in
+instance [BroadcastType tag R ι X MX] [BroadcastType tag R ι Y MY] : BroadcastType tag R ι (X×Y) (MX×MY) where
+  equiv := {
+    toFun  := fun (mx,my) i => (equiv tag (R:=R) mx i, 
+                                equiv tag (R:=R) my i)
+    invFun := fun xy => ((equiv tag (R:=R)).invFun fun i => (xy i).1, 
+                         (equiv tag (R:=R)).invFun fun i => (xy i).2) 
+    map_add'  := by intro x y; funext i; simp
+    map_smul' := by intro x y; funext i; simp
+    left_inv  := fun _ => by simp
+    right_inv := fun _ => by simp
+  }
+
+open BroadcastType in
+instance [∀ j, BroadcastType tag R ι (E j) (ME j)]
+  : BroadcastType tag R ι (∀ j, E j) (∀ j, ME j) where
+  equiv := {
+    toFun  := fun mx i j => equiv tag (R:=R) (mx j) i 
+    invFun := fun x j => (equiv tag (R:=R)).invFun (fun i => x i j)
+    map_add'  := by intro x y; funext i j; simp
+    map_smul' := by intro x y; funext i j; simp
+    left_inv  := fun _ => by simp
+    right_inv := fun _ => by simp
+  }
+
+open BroadcastType in
+instance : BroadcastType `normal R Unit X X where
+  equiv := {
+    toFun  := fun x _ => x
+    invFun := fun x => x ()
+    map_add'  := by intro x y; funext _; simp
+    map_smul' := by intro x y; funext _; simp
+    left_inv  := fun _ => by simp
+    right_inv := fun _ => by simp
+  }
+
+-- open BroadcastType in
+-- instance [BroadcastType `normal R (Fin n) X MX] : BroadcastType `normal R (Fin (n+1)) X (X×MX) where
+--   equiv := {
+--     toFun  := fun (x,mx) i =>
+--       match i with
+--       | ⟨0, _⟩ => x
+--       | ⟨i'+1, h⟩ => 
+--         let i' : Fin n := ⟨i', by aesop⟩
+--         equiv `normal (R:=R) mx i'
+--     invFun := fun x => (x 0, (equiv `normal (R:=R)).invFun fun i : Fin n => x ⟨i.1+1, by aesop⟩)
+--     map_add'  := by intro x y; funext ⟨i,hi⟩; induction i; simp; rfl; simp
+--     map_smul' := by intro x y; funext ⟨i,hi⟩; induction i; simp; rfl; simp
+--     left_inv  := fun (x,mx) => by simp; rfl
+--     right_inv := fun _ => by simp; funext ⟨i,hi⟩; induction i; simp; rfl
+--   }
+
+
+-- instance : Broadcast `EigenSparse ℝ^m (Eigen.SparseMatrix n m) (Fin n) where
+-- instance : Broadcast `EigenDense ℝ^m (Eigen.Matrix n m) (Fin n) where
+
+
+noncomputable
+def fwdDeriv
+  (K : Type _) [NontriviallyNormedField K]
+  (tag : Name) (ι : Type _)
+  {X : Type _} [NormedAddCommGroup X] [NormedSpace K X]
+  {Y : Type _} [NormedAddCommGroup Y] [NormedSpace K Y]
+  {DX : Type _} [AddCommGroup DX] [Module K DX]
+  {DY : Type _} [AddCommGroup DY] [Module K DY]
+  [BroadcastType tag K ι X DX] [BroadcastType tag K ι Y DY]
+  (f : X → Y) (x : X) (dx : DX) : Y×DY :=
+  (f x, broadcast tag (R:=K) (ι:=ι) (fun dx => fderiv K f x dx) dx)
+
+namespace fwdDeriv
+
+variable
+  {K : Type _} [NontriviallyNormedField K]
+  {tag : Name} {ι : Type _}
+  {X : Type _} [NormedAddCommGroup X] [NormedSpace K X]
+  {Y : Type _} [NormedAddCommGroup Y] [NormedSpace K Y]
+  {Z : Type _} [NormedAddCommGroup Z] [NormedSpace K Z]
+  {DX : Type _} [AddCommGroup DX] [Module K DX] [BroadcastType tag K ι X DX]
+  {DY : Type _} [AddCommGroup DY] [Module K DY] [BroadcastType tag K ι Y DY]
+  {DZ : Type _} [AddCommGroup DZ] [Module K DZ] [BroadcastType tag K ι Z DZ]
+  {κ : Type _} [Fintype κ]
+  {E : κ → Type _} [∀ j, NormedAddCommGroup (E j)] [∀ j, NormedSpace K (E j)]
+  {DE : κ → Type _} [∀ j, AddCommGroup (DE j)] [∀ j, Module K (DE j)]
+  [∀ j, BroadcastType tag K ι (E j) (DE j)]
+  
+
+theorem id_rule 
+  : fwdDeriv K tag ι (fun x : X => x) = fun x dx => (x,dx) :=
+by
+  unfold fwdDeriv; unfold broadcast
+  simp
+
+theorem const_rule (x :X)
+  : fwdDeriv K tag ι (fun y : Y => x) = fun y dy => (x, 0) :=
+by
+  unfold fwdDeriv; unfold broadcast
+  funext y dy
+  simp; rfl
+
+theorem comp_rule 
+  (g : X → Y) (hg : Differentiable K g)
+  (f : Y → Z) (hf : Differentiable K f)
+  : fwdDeriv K tag ι (fun x : X => f (g x)) 
+    = 
+    fun x dx => 
+      let ydy := fwdDeriv K tag ι g x dx 
+      let zdz := fwdDeriv K tag ι f ydy.1 ydy.2 
+      zdz :=
+by
+  unfold fwdDeriv; unfold broadcast
+  funext x dx; congr; funext i;
+  rw[fderiv.comp_rule g hg f hf]
+  simp
+
+
+theorem let_rule 
+  (g : X → Y) (hg : Differentiable K g)
+  (f : X → Y → Z) (hf : Differentiable K (fun (xy : X×Y) => f xy.1 xy.2))
+  : fwdDeriv K tag ι (fun x : X => let y := g x; f x y) 
+    = 
+    fun x dx => 
+      let ydy := fwdDeriv K tag ι g x dx 
+      let zdz := fwdDeriv K tag ι (fun (xy : X×Y) => f xy.1 xy.2) (x,ydy.1) (dx,ydy.2)
+      zdz :=
+by
+  unfold fwdDeriv; unfold broadcast
+  funext x dx; congr; funext i
+  rw[fderiv.let_rule g hg f hf]; 
+  simp; congr; simp
+
+
+
+theorem pi_rule
+  (f : (j : κ) → X → E j) (hf : ∀ j, Differentiable K (f j))
+  : (fwdDeriv K tag ι fun (x : X) (j : κ) => f j x)
+    = 
+    fun x dx =>
+      (fun j => f j x, fun j => (fwdDeriv K tag ι (f j) x dx).2) := 
+by 
+  unfold fwdDeriv; unfold broadcast
+  funext x; rw[fderiv_pi (fun i => hf i x)]
+  simp; funext dx; simp[BroadcastType.equiv]
+
+
+-- Register `fwdDeriv` as function transformation ------------------------------
+--------------------------------------------------------------------------------
+
+open Lean Meta Qq
+
+def fwdDeriv.discharger (e : Expr) : SimpM (Option Expr) := do
+  withTraceNode `fwdDeriv_discharger (fun _ => return s!"discharge {← ppExpr e}") do
+  let cache := (← get).cache
+  let config : FProp.Config := {}
+  let state  : FProp.State := { cache := cache }
+  let (proof?, state) ← FProp.fprop e |>.run config |>.run state
+  modify (fun simpState => { simpState with cache := state.cache })
+  return proof?
+
+open Lean Elab Term FTrans
+def fwdDeriv.ftransExt : FTransExt where
+  ftransName := ``fwdDeriv
+
+  getFTransFun? e := 
+    if e.isAppOf ``fwdDeriv then
+
+      if let .some f := e.getArg? 19 then
+        some f
+      else 
+        none
+    else
+      none
+
+  replaceFTransFun e f := 
+    if e.isAppOf ``fwdDeriv then
+      e.modifyArg (fun _ => f) 19
+    else          
+      e
+
+  identityRule     := .some <| .thm ``id_rule
+  constantRule     := .some <| .thm ``const_rule
+  compRule         := .some <| .thm ``comp_rule
+  lambdaLetRule    := .some <| .thm ``let_rule
+  lambdaLambdaRule := .some <| .thm ``pi_rule
+
+  discharger := fwdDeriv.discharger
+
+
+-- register fderiv
+#eval show Lean.CoreM Unit from do
+  modifyEnv (λ env => FTrans.ftransExt.addEntry env (``fwdDeriv, fwdDeriv.ftransExt))
+
+
+example : BroadcastType tag K ι X DX := by infer_instance
+
+
+@[ftrans_rule]
+theorem HAdd.hAdd.arg_a4a5.fderiv_comp 
+  (f g : X → Y) (hf : Differentiable K f) (hg : Differentiable K g)
+  : (fwdDeriv K tag ι fun x => f x + g x)
+    =
+    fun x dx => 
+      let ydy₁ := fwdDeriv K tag ι f x dx
+      let ydy₂ := fwdDeriv K tag ι g x dx
+      ydy₁ + ydy₂ := 
+by 
+  funext x dx
+  unfold fwdDeriv; unfold broadcast
+  ftrans only
+  simp; rw[← map_add]; rfl
+
+
diff --git a/SciLean/FTrans/FwdDeriv/Test.lean b/SciLean/FTrans/FwdDeriv/Test.lean
new file mode 100644
index 00000000..37e18e47
--- /dev/null
+++ b/SciLean/FTrans/FwdDeriv/Test.lean
@@ -0,0 +1,35 @@
+import SciLean.FTrans.FwdDeriv.Basic
+
+import SciLean.Tactic.LSimp.Notation
+import SciLean.Tactic.LetEnter
+import SciLean.Tactic.Basic
+
+
+open SciLean
+
+variable
+  {K : Type _} [NontriviallyNormedField K] 
+
+example
+  : fwdDeriv K `normal Unit (fun x : K => x + x + x + x + x)
+    =
+    fun x dx => 
+     (x + x + x + x + x, dx + dx + dx + dx + dx):= 
+by
+  conv =>
+    lhs
+    ftrans only
+    enter [x,dx]
+    simp (config := { zeta := false}) only [Prod.add_def]
+    ftrans only
+  
+#exit
+
+example
+  : fwdDeriv K `normal Unit (fun x : K => x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x)
+    =
+    fun x dx => 
+     (x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x, 
+      dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx + dx):= 
+by
+  ftrans
diff --git a/SciLean/FunctionSpaces/Differentiable/Tactic.lean b/SciLean/FunctionSpaces/Differentiable/Tactic.lean
index b366662c..4a95e5dc 100644
--- a/SciLean/FunctionSpaces/Differentiable/Tactic.lean
+++ b/SciLean/FunctionSpaces/Differentiable/Tactic.lean
@@ -145,8 +145,4 @@ theorem hoho : Differentiable ℝ (fun x : ℝ => let y := x + x + x + x + x + (
 
 example : Differentiable ℝ (fun x : ℝ => x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x) := by fprop
 
-example : Differentiable ℝ (fun x : ℝ => x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x + x) := by differentiable
-
-example : Differentiable ℝ (fun x : ℝ => let y := x + x; let z := x + y; let f := fun x : ℝ => x + x; f y + y + x + z) := by differentiable
-
 
diff --git a/SciLean/Tactic/FProp/Basic.lean b/SciLean/Tactic/FProp/Basic.lean
index b1db5eb2..d63cdeb8 100644
--- a/SciLean/Tactic/FProp/Basic.lean
+++ b/SciLean/Tactic/FProp/Basic.lean
@@ -77,7 +77,7 @@ def cache (e : Expr) (proof? : Option Expr) : FPropM (Option Expr) := -- return
   match proof? with
   | .none => return none
   | .some proof => do
-    modify (fun s => { s with cache := s.cache.insert e proof} )
+    modify (fun s => { s with cache := s.cache.insert e { expr := q(True), proof? := proof} })
     return proof
 
 
@@ -90,10 +90,6 @@ def getLocalRules (fpropName : Name) : MetaM (Array SimpTheorem) := do
     
     if (type.getForallBody.getAppFn.constName? == .some fpropName) &&
        (var.kind ≠ Lean.LocalDeclKind.auxDecl) then
-       -- dbg_trace "adding `{← ppExpr var.toExpr} : {←ppExpr type}` to local rules to be applied"
-       -- dbg_trace "hasExprMVar {var.hasExprMVar}"
-       -- dbg_trace "hasValue {var.hasValue}"
-       -- dbg_trace "hasValue {repr var.kind}"
        arr := arr.push {
          proof := var.toExpr
          origin := .fvar var.fvarId
@@ -106,7 +102,8 @@ def getLocalRules (fpropName : Name) : MetaM (Array SimpTheorem) := do
 mutual 
   partial def fprop (e : Expr) : FPropM (Option Expr) := do
 
-    if let .some proof := (← get).cache.find? e then
+    if let .some { expr := _, proof? := .some proof } := (← get).cache.find? e then
+      trace[Meta.Tactic.fprop.cache] "cached result for {e}"
       return proof
     else
       forallTelescope e fun xs b => do
@@ -131,16 +128,22 @@ mutual
       ext.identityRule e
 
     | .lam xName xType (.letE yName yType yValue body _) xBi => 
+      -- We perform reduction because the type is quite often of the form 
+      -- `(fun x => Y) #0` which is just `Y`
+      let yType := yType.headBeta
+      if (yType.hasLooseBVar 0) then
+        throwError "dependent type encountered {← ppExpr (Expr.forallE xName xType yType default)}"
+
       match (body.hasLooseBVar 0), (body.hasLooseBVar 1) with
       | true, true =>
         trace[Meta.Tactic.fprop.step] "case let\n{← ppExpr e}"
-        let f := Expr.lam xName xType (.lam yName yType body xBi) default
+        let f := Expr.lam xName xType (.lam yName yType body default) xBi
         let g := Expr.lam xName xType yValue default
         ext.lambdaLetRule e f g
 
       | true, false => 
         trace[Meta.Tactic.fprop.step] "case comp\n{← ppExpr e}"
-        let f := Expr.lam yName yType body xBi
+        let f := Expr.lam yName yType body default
         let g := Expr.lam xName xType yValue default
         ext.compRule e f g
 
@@ -148,6 +151,7 @@ mutual
         let f := Expr.lam xName xType (body.lowerLooseBVars 1 1) xBi
         FProp.fprop (ext.replaceFPropFun e f)
 
+
     | .lam _ _ (.lam  ..) _ => 
       trace[Meta.Tactic.fprop.step] "case pi\n{← ppExpr e}"
       ext.lambdaLambdaRule e f
@@ -160,11 +164,14 @@ mutual
         trace[Meta.Tactic.fprop.step] "case fvar app\n{← ppExpr e}"
         applyFVarApp e ext.discharger
       else
-        trace[Meta.Tactic.fprop.step] "case other\n{← ppExpr e}"
+        trace[Meta.Tactic.fprop.step] "case other\n{← ppExpr e}\n"
         applyTheorems e (ext.discharger)
 
+    | .mvar _ => do
+      fprop (← instantiateMVars e)
+
     | _ => do
-      trace[Meta.Tactic.fprop.step] "case other\n{← ppExpr e}"
+      trace[Meta.Tactic.fprop.step] "case other\n{← ppExpr e}\n"
       applyTheorems e (ext.discharger)
 
   partial def applyFVarApp (e : Expr) (discharge? : Expr → FPropM (Option Expr)) : FPropM (Option Expr) := do
diff --git a/SciLean/Tactic/FProp/Init.lean b/SciLean/Tactic/FProp/Init.lean
index 51e92ab8..09e2ee09 100644
--- a/SciLean/Tactic/FProp/Init.lean
+++ b/SciLean/Tactic/FProp/Init.lean
@@ -18,6 +18,7 @@ namespace SciLean.FProp
 -------------
 initialize registerTraceClass `Meta.Tactic.fprop
 initialize registerTraceClass `Meta.Tactic.fprop.step
+initialize registerTraceClass `Meta.Tactic.fprop.cache
 initialize registerTraceClass `Meta.Tactic.fprop.missing_rule
 -- initialize registerTraceClass `Meta.Tactic.fprop.normalize_let
 initialize registerTraceClass `Meta.Tactic.fprop.rewrite
@@ -33,10 +34,11 @@ open Meta
 structure Config where
   -- config
 
-abbrev Cache := ExprMap Expr
+-- abbrev Cache := ExprMap Expr
 
 structure State where
-  cache        : Cache := {}
+  /-- Simp's cache is used as the `fprop` tactic is designed to be used inside of simp and utilize its cache -/
+  cache        : Simp.Cache := {}
 
 abbrev _root_.SciLean.FPropM := ReaderT FProp.Config $ StateRefT FProp.State MetaM
 
diff --git a/SciLean/Tactic/FTrans/Init.lean b/SciLean/Tactic/FTrans/Init.lean
index de7ba2b9..6168bccc 100644
--- a/SciLean/Tactic/FTrans/Init.lean
+++ b/SciLean/Tactic/FTrans/Init.lean
@@ -73,6 +73,8 @@ structure FTransExt where
   identityRule     : Option RewriteRule
   /-- Custom rule for transforming `fun x => y -/
   constantRule    : Option RewriteRule
+  /-- Custom rule for transforming `fun x => f (g x)` or `fun x => let y := g x; f y -/
+  compRule    : Option RewriteRule
   /-- Custom rule for transforming `fun x => let y := g x; f x y -/
   lambdaLetRule    : Option RewriteRule
   /-- Custom rule for transforming `fun x y => f x y -/