diff --git a/SciLean.lean b/SciLean.lean
index 987b079f..e70ca6e0 100644
--- a/SciLean.lean
+++ b/SciLean.lean
@@ -8,7 +8,10 @@ import SciLean.Data.DataArray
 import SciLean.Functions.OdeSolve
 import SciLean.Solver.Solver 
 
+import SciLean.Tactic.FTrans.Basic
+import SciLean.Tactic.FProp.Notation
 import SciLean.FTrans.FDeriv.Basic
+import SciLean.FunctionSpaces.Differentiable.Basic
 
 /-!
 
diff --git a/SciLean/FunctionSpaces/Continuous/Basic.lean b/SciLean/FunctionSpaces/Continuous/Basic.lean
new file mode 100644
index 00000000..b665f060
--- /dev/null
+++ b/SciLean/FunctionSpaces/Continuous/Basic.lean
@@ -0,0 +1,300 @@
+import Mathlib.Topology.Basic
+import Mathlib.Topology.Constructions
+import Mathlib.Topology.Algebra.Group.Basic
+import Mathlib.Topology.Algebra.GroupWithZero
+
+import Mathlib.Analysis.Calculus.FDeriv.Basic
+
+import SciLean.Tactic.FProp.Basic
+import SciLean.Tactic.FProp.Notation
+
+namespace SciLean
+
+
+-- Basic rules -----------------------------------------------------------------
+--------------------------------------------------------------------------------
+
+namespace Continuous
+
+variable 
+  {X : Type _} [TopologicalSpace X]
+  {Y : Type _} [TopologicalSpace Y]
+  {Z : Type _} [TopologicalSpace Z]
+  {ι : Type _} [Fintype ι]
+  {E : ι → Type _} [∀ i, TopologicalSpace  (E i)]
+  
+
+theorem id_rule
+  : Continuous (fun x : X => x)
+  := by continuity
+  
+
+theorem const_rule (x : X)
+  : Continuous (fun _ : Y => x)
+  := by continuity
+
+
+theorem comp_rule
+  (g : X → Y) (hg : Continuous g)
+  (f : Y → Z) (hf : Continuous f)
+  : Continuous (fun x => f (g x))
+  := Continuous.comp hf hg
+
+
+theorem let_rule
+  (g : X → Y) (hg : Continuous g)
+  (f : X → Y → Z) (hf : Continuous (fun (xy : X×Y) => f xy.1 xy.2))
+  : Continuous (fun x => let y := g x; f x y) 
+  := by 
+  rw[(by rfl : (fun x => let y := g x; f x y) = (fun (xy : X×Y) => f xy.1 xy.2)∘(fun x => (x,g x)))]
+  apply (Continuous.comp hf (by continuity))
+
+
+theorem pi_rule
+  (f : (i : ι) → X → E i) (hf : ∀ i, Continuous (f i))
+  : Continuous (fun x i => f i x)
+  := by continuity
+
+
+end SciLean.Continuous
+
+
+--------------------------------------------------------------------------------
+-- Register Diferentiable ------------------------------------------------------
+--------------------------------------------------------------------------------
+
+open Lean Meta SciLean FProp
+def Continuous.fpropExt : FPropExt where
+  fpropName := ``Continuous
+  getFPropFun? e := 
+    if e.isAppOf ``Continuous then
+
+      if let .some f := e.getArg? 4 then
+        some f
+      else 
+        none
+    else
+      none
+
+  replaceFPropFun e f := 
+    if e.isAppOf ``Continuous then
+      e.modifyArg (fun _ => f) 4 
+    else          
+      e
+
+  identityRule    e :=
+    let thm : SimpTheorem :=
+    {
+      proof  := mkConst ``Continuous.id_rule 
+      origin := .decl ``Continuous.id_rule 
+      rfl    := false
+    }
+    FProp.tryTheorem? e thm (fun _ => pure none)
+
+  constantRule e :=
+    let thm : SimpTheorem :=
+    {
+      proof  := mkConst ``Continuous.const_rule 
+      origin := .decl ``Continuous.const_rule 
+      rfl    := false
+    }
+    FProp.tryTheorem? e thm (fun _ => pure none)
+
+  compRule _ f g := do
+    let HF ← mkAppM ``Continuous #[f]
+    let .some hf ← FProp.fprop HF
+      | trace[Meta.Tactic.fprop.discharge] "failed to prove {HF}"
+        return none
+
+    let HG ← mkAppM ``Continuous #[g]
+    let .some hg ← FProp.fprop HG
+      | trace[Meta.Tactic.fprop.discharge] "failed to prove {HG}"
+        return none
+
+    mkAppM ``Continuous.comp_rule #[g,hg,f,hf]
+
+  lambdaLetRule _ f g := do
+    -- let thm : SimpTheorem :=
+    -- {
+    --   proof  := mkConst ``Continuous.let_rule 
+    --   origin := .decl ``Continuous.let_rule 
+    --   rfl    := false
+    -- }
+    -- FProp.tryTheorem? e thm (fun _ => pure none)
+
+    let HF ← mkAppM ``Continuous #[(← mkUncurryFun 2 f)]
+    let .some hf ← FProp.fprop HF
+      | trace[Meta.Tactic.fprop.discharge] "failed to prove {HF}"
+        return none
+
+    let HG ← mkAppM ``Continuous #[g]
+    let .some hg ← FProp.fprop HG
+      | trace[Meta.Tactic.fprop.discharge] "failed to prove {HG}"
+        return none
+
+    mkAppM ``Continuous.let_rule #[g,hg,f,hf]
+
+  lambdaLambdaRule e _ :=
+    let thm : SimpTheorem :=
+    {
+      proof  := mkConst ``Continuous.pi_rule 
+      origin := .decl ``Continuous.pi_rule 
+      rfl    := false
+    }
+    FProp.tryTheorem? e thm (fun _ => pure none)
+
+  discharger _ := return none
+
+-- register fderiv
+#eval show Lean.CoreM Unit from do
+  modifyEnv (λ env => FProp.fpropExt.addEntry env (``Continuous, Continuous.fpropExt))
+
+
+
+--------------------------------------------------------------------------------
+-- Function Rules --------------------------------------------------------------
+--------------------------------------------------------------------------------
+
+open SciLean Continuous 
+
+variable 
+  {X : Type _} [TopologicalSpace X]
+  {Y : Type _} [TopologicalSpace Y]
+  {Z : Type _} [TopologicalSpace Z]
+  {R : Type _} [TopologicalSpace R]
+  {ι : Type _} [Fintype ι]
+  {E : ι → Type _} [∀ i, TopologicalSpace  (E i)]
+
+
+-- Id --------------------------------------------------------------------------
+--------------------------------------------------------------------------------
+
+
+@[fprop_rule]
+theorem id.arg_a.Continuous
+  : Continuous (id : X → X) := by continuity
+
+
+-- Prod ------------------------------------------------------------------------
+--------------------------------------------------------------------------------
+
+-- Prod.mk --------------------------------------------------------------------
+--------------------------------------------------------------------------------
+
+@[fprop_rule]
+theorem Prod.mk.arg_fstsnd.Continuous_comp
+  (g : X → Y) (hg : Continuous g)
+  (f : X → Z) (hf : Continuous f)
+  : Continuous fun x => (g x, f x)
+  := by continuity
+
+
+
+-- Prod.fst --------------------------------------------------------------------
+--------------------------------------------------------------------------------
+
+@[fprop_rule]
+theorem Prod.fst.arg_self.Continuous_comp 
+  (f : X → Y×Z) (hf : Continuous f)
+  : Continuous (fun x => (f x).1)
+  := Continuous.fst hf
+
+
+
+-- Prod.snd --------------------------------------------------------------------
+--------------------------------------------------------------------------------
+
+@[fprop_rule]
+theorem Prod.snd.arg_self.Continuous_comp 
+  (f : X → Y×Z) (hf : Continuous f)
+  : Continuous (fun x => (f x).2)
+  := Continuous.snd hf
+
+
+
+-- Function.comp ---------------------------------------------------------------
+--------------------------------------------------------------------------------
+
+@[fprop_rule]
+theorem Function.comp.arg_x.Continuous_comp
+  (f : Y → Z) (hf : Continuous f)
+  (g : X → Y) (hg : Continuous g)
+  : Continuous (f ∘ g)
+  := Continuous.comp hf hg
+
+
+
+-- Neg.neg ---------------------------------------------------------------------
+--------------------------------------------------------------------------------
+
+@[fprop_rule]
+theorem Neg.neg.arg_a2.Continuous_comp
+  [Neg Y] [ContinuousNeg Y]
+  (f : X → Y) (hf : Continuous f) 
+  : Continuous fun x => - f x 
+  := by continuity
+
+
+
+-- HAdd.hAdd -------------------------------------------------------------------
+--------------------------------------------------------------------------------
+
+@[fprop_rule]
+theorem HAdd.hAdd.arg_a4a5.Continuous_comp
+  [Add Y] [ContinuousAdd Y]
+  (f g : X → Y) (hf : Continuous f) (hg : Continuous g)
+  : Continuous fun x => f x + g x
+  := by continuity
+
+
+
+-- HSub.hSub -------------------------------------------------------------------
+--------------------------------------------------------------------------------
+
+@[fprop_rule]
+theorem HSub.hSub.arg_a4a5.Continuous_comp
+  [Sub Y] [ContinuousSub Y]
+  (f g : X → Y) (hf : Continuous f) (hg : Continuous g)
+  : Continuous fun x => f x - g x
+  := by continuity
+
+
+
+-- HMul.hMul ---------------------------------------------------------------------
+-------------------------------------------------------------------------------- 
+
+@[fprop_rule]
+def HMul.hMul.arg_a4a5.Continuous_comp
+  [Mul Y] [ContinuousMul Y]
+  (f g : X → Y) (hf : Continuous f) (hg : Continuous g)
+  : Continuous (fun x => f x * g x)
+  := Continuous.mul hf hg
+
+
+
+-- SMul.sMul ---------------------------------------------------------------------
+-------------------------------------------------------------------------------- 
+
+@[fprop_rule]
+def SMul.sMul.arg_a4a5.Continuous_comp
+  [SMul R Y] [ContinuousSMul R Y]
+  (f : X → R) (g : X → Y) (hf : Continuous f) (hg : Continuous g)
+  : Continuous (fun x => f x • g x)
+  := Continuous.smul hf hg
+
+
+
+-- HDiv.hDiv ---------------------------------------------------------------------
+-------------------------------------------------------------------------------- 
+
+
+@[fprop_rule]
+def HDiv.hDiv.arg_a4a5.Continuous_comp
+  [GroupWithZero K] [TopologicalSpace K] [ContinuousMul K] [HasContinuousInv₀ K]
+  (f : R → K) (g : R → K) 
+  (hf : Continuous f) (hg : Continuous g) (hx : ∀ x, g x ≠ 0)
+  : Continuous (fun x => f x / g x)
+  := Continuous.div hf hg hx
+
+
+
diff --git a/SciLean/FunctionSpaces/Continuous/Test.lean b/SciLean/FunctionSpaces/Continuous/Test.lean
new file mode 100644
index 00000000..ee0b07fd
--- /dev/null
+++ b/SciLean/FunctionSpaces/Continuous/Test.lean
@@ -0,0 +1,26 @@
+import SciLean.FunctionSpaces.Continuous.Basic
+import SciLean.Profile
+
+set_option profiler true
+set_option profiler.threshold 10
+
+example : Continuous (fun x : ℝ => 
+  let x1 := x
+  let x2 := x + x1
+  let x3 := x + x1 + x2
+  let x4 := x + x1 + x2 + x3
+  let x5 := x + x1 + x2 + x3 + x4
+  let x6 := x + x1 + x2 + x3 + x4 + x5
+  let x7 := x + x1 + x2 + x3 + x4 + x5 + x6
+  x7) := by fprop
+
+
+example : Continuous (fun x : ℝ => 
+  let x1 := x
+  let x2 := x + x1
+  let x3 := x + x1 + x2
+  let x4 := x + x1 + x2 + x3
+  let x5 := x + x1 + x2 + x3 + x4
+  let x6 := x + x1 + x2 + x3 + x4 + x5
+  let x7 := x + x1 + x2 + x3 + x4 + x5 + x6
+  x7) := by continuity
diff --git a/SciLean/FunctionSpaces/Differentiable/Basic.lean b/SciLean/FunctionSpaces/Differentiable/Basic.lean
index 0d7978e4..3b12956c 100644
--- a/SciLean/FunctionSpaces/Differentiable/Basic.lean
+++ b/SciLean/FunctionSpaces/Differentiable/Basic.lean
@@ -6,8 +6,9 @@ import Mathlib.Analysis.Calculus.FDeriv.Add
 import Mathlib.Analysis.Calculus.FDeriv.Mul
 import Mathlib.Analysis.Calculus.Deriv.Inv
 
-
 import SciLean.FunctionSpaces.Differentiable.Init
+import SciLean.Tactic.FProp.Basic
+
 
 namespace SciLean
 
@@ -148,6 +149,103 @@ theorem pi_rule
 end SciLean.Differentiable
 
 
+--------------------------------------------------------------------------------
+-- Register Diferentiable ------------------------------------------------------
+--------------------------------------------------------------------------------
+
+open Lean Meta SciLean FProp
+def Differentiable.fpropExt : FPropExt where
+  fpropName := ``Differentiable
+  getFPropFun? e := 
+    if e.isAppOf ``Differentiable then
+
+      if let .some f := e.getArg? 8 then
+        some f
+      else 
+        none
+    else
+      none
+
+  replaceFPropFun e f := 
+    if e.isAppOf ``Differentiable then
+      e.modifyArg (fun _ => f) 8 
+    else          
+      e
+
+  identityRule    e :=
+    let thm : SimpTheorem :=
+    {
+      proof  := mkConst ``Differentiable.id_rule 
+      origin := .decl ``Differentiable.id_rule 
+      rfl    := false
+    }
+    FProp.tryTheorem? e thm (fun _ => pure none)
+
+  constantRule    e :=
+    let thm : SimpTheorem :=
+    {
+      proof  := mkConst ``Differentiable.const_rule 
+      origin := .decl ``Differentiable.const_rule 
+      rfl    := false
+    }
+    FProp.tryTheorem? e thm (fun _ => pure none)
+
+  compRule e f g := do
+    let .some R := e.getArg? 0
+      | return none
+
+    let HF ← mkAppM ``Differentiable #[R, f]
+    let .some hf ← FProp.fprop HF
+      | trace[Meta.Tactic.fprop.discharge] "Differentiable.comp_rule, failed to discharge hypotheses{HF}"
+        return none
+
+    let HG ← mkAppM ``Differentiable #[R, g]
+    let .some hg ← FProp.fprop HG
+      | trace[Meta.Tactic.fprop.discharge] "Differentiable.comp_rule, failed to discharge hypotheses{HG}"
+        return none
+
+    mkAppM ``Differentiable.let_rule #[g,hg,f,hf]
+
+  lambdaLetRule e f g := do
+    -- let thm : SimpTheorem :=
+    -- {
+    --   proof  := mkConst ``Differentiable.let_rule 
+    --   origin := .decl ``Differentiable.let_rule 
+    --   rfl    := false
+    -- }
+    -- FProp.tryTheorem? e thm (fun _ => pure none)
+    let .some R := e.getArg? 0
+      | return none
+
+    let HF ← mkAppM ``Differentiable #[R, (← mkUncurryFun 2 f)]
+    let .some hf ← FProp.fprop HF
+      | trace[Meta.Tactic.fprop.discharge] "Differentiable.let_rule, failed to discharge hypotheses{HF}"
+        return none
+
+    let HG ← mkAppM ``Differentiable #[R, g]
+    let .some hg ← FProp.fprop HG
+      | trace[Meta.Tactic.fprop.discharge] "Differentiable.let_rule, failed to discharge hypotheses{HG}"
+        return none
+
+    mkAppM ``Differentiable.let_rule #[g,hg,f,hf]
+
+  lambdaLambdaRule e _ :=
+    let thm : SimpTheorem :=
+    {
+      proof  := mkConst ``Differentiable.pi_rule 
+      origin := .decl ``Differentiable.pi_rule 
+      rfl    := false
+    }
+    FProp.tryTheorem? e thm (fun _ => pure none)
+
+  discharger _ := return none
+
+-- register fderiv
+#eval show Lean.CoreM Unit from do
+  modifyEnv (λ env => FProp.fpropExt.addEntry env (``Differentiable, Differentiable.fpropExt))
+
+
+
 --------------------------------------------------------------------------------
 -- Function Rules --------------------------------------------------------------
 --------------------------------------------------------------------------------
@@ -171,7 +269,7 @@ theorem id.arg_a.DifferentiableAt (x : X)
   : DifferentiableAt R (id : X → X) x := by simp
 
 
-@[differentiable]
+@[differentiable, fprop_rule]
 theorem id.arg_a.Differentiable
   : Differentiable R (id : X → X) := by simp
 
@@ -191,7 +289,7 @@ theorem Prod.mk.arg_fstsnd.DifferentiableAt_comp
   := DifferentiableAt.prod hg hf
 
 
-@[differentiable]
+@[differentiable, fprop_rule]
 theorem Prod.mk.arg_fstsnd.Differentiable_comp
   (g : X → Y) (hg : Differentiable R g)
   (f : X → Z) (hf : Differentiable R f)
@@ -211,7 +309,7 @@ theorem Prod.fst.arg_self.DifferentiableAt_comp
   := DifferentiableAt.fst hf
 
 
-@[differentiable]
+@[differentiable, fprop_rule]
 theorem Prod.fst.arg_self.Differentiable_comp 
   (f : X → Y×Z) (hf : Differentiable R f)
   : Differentiable R (fun x => (f x).1)
@@ -230,7 +328,7 @@ theorem Prod.snd.arg_self.DifferentiableAt_comp
   := DifferentiableAt.snd hf
 
 
-@[differentiable]
+@[differentiable, fprop_rule]
 theorem Prod.snd.arg_self.Differentiable_comp 
   (f : X → Y×Z) (hf : Differentiable R f)
   : Differentiable R (fun x => (f x).2)
@@ -238,6 +336,18 @@ theorem Prod.snd.arg_self.Differentiable_comp
 
 
 
+-- Function.comp ---------------------------------------------------------------
+--------------------------------------------------------------------------------
+
+@[fprop_rule]
+theorem Function.comp.arg_x.Differentiable_comp
+  (f : Y → Z) (hf : Differentiable R f)
+  (g : X → Y) (hg : Differentiable R g)
+  : Differentiable R (f ∘ g)
+  := Differentiable.comp hf hg
+
+
+
 -- Neg.neg ---------------------------------------------------------------------
 --------------------------------------------------------------------------------
 
@@ -248,7 +358,7 @@ theorem Neg.neg.arg_a2.DifferentiableAt_comp
   := DifferentiableAt.neg hf
  
 
-@[differentiable]
+@[differentiable, fprop_rule]
 theorem Neg.neg.arg_a2.Differentiable_comp
   (f : X → Y) (hf : Differentiable R f) 
   : Differentiable R fun x => - f x 
@@ -266,7 +376,7 @@ theorem HAdd.hAdd.arg_a4a5.DifferentiableAt_comp
   := DifferentiableAt.add hf hg
  
 
-@[differentiable]
+@[differentiable, fprop_rule]
 theorem HAdd.hAdd.arg_a4a5.Differentiable_comp
   (f g : X → Y) (hf : Differentiable R f) (hg : Differentiable R g)
   : Differentiable R fun x => f x + g x
@@ -284,7 +394,7 @@ theorem HSub.hSub.arg_a4a5.DifferentiableAt_comp
   := DifferentiableAt.sub hf hg
  
 
-@[differentiable]
+@[differentiable, fprop_rule]
 theorem HSub.hSub.arg_a4a5.Differentiable_comp
   (f g : X → Y) (hf : Differentiable R f) (hg : Differentiable R g)
   : Differentiable R fun x => f x - g x
@@ -303,7 +413,7 @@ def HMul.hMul.arg_a4a5.DifferentiableAt_comp
   := DifferentiableAt.mul hf hg
 
 
-@[differentiable]
+@[differentiable, fprop_rule]
 def HMul.hMul.arg_a4a5.Differentiable_comp
   {Y : Type _} [TopologicalSpace Y] [NormedRing Y] [NormedAlgebra R Y] 
   (f g : X → Y) (hf : Differentiable R f) (hg : Differentiable R g)
@@ -323,7 +433,7 @@ def SMul.sMul.arg_a4a5.DifferentiableAt_comp
   := DifferentiableAt.smul hf hg
 
 
-@[differentiable]
+@[differentiable, fprop_rule]
 def SMul.sMul.arg_a4a5.Differentiable_comp
   {Y : Type _} [TopologicalSpace Y] [NormedRing Y] [NormedAlgebra R Y] 
   (f : X → R) (g : X → Y) (hf : Differentiable R f) (hg : Differentiable R g)
@@ -345,7 +455,7 @@ def HDiv.hDiv.arg_a4a5.DifferentiableAt_comp
   := DifferentiableAt.div hf hg hx
 
 
-@[differentiable]
+@[differentiable, fprop_rule]
 def HDiv.hDiv.arg_a4a5.Differentiable_comp
   {R : Type _} [NontriviallyNormedField R]
   {K : Type _} [NontriviallyNormedField K] [NormedAlgebra R K]
diff --git a/SciLean/FunctionSpaces/Differentiable/Tactic.lean b/SciLean/FunctionSpaces/Differentiable/Tactic.lean
index 5eb7c22d..510c22d1 100644
--- a/SciLean/FunctionSpaces/Differentiable/Tactic.lean
+++ b/SciLean/FunctionSpaces/Differentiable/Tactic.lean
@@ -2,93 +2,9 @@ import SciLean.Tactic.FProp.Basic
 import SciLean.Tactic.FProp.Notation
 
 import SciLean.FunctionSpaces.Differentiable.Basic
-import SciLean.Profile
 
 set_option profiler true
-
---------------------------------------------------------------------------------
---------------------------------------------------------------------------------
-
-open SciLean Lean Meta Qq
-
-
-def Differentiable.discharger (e : Expr) : SimpM (Option Expr) := do
-  return none
-
-
-open Lean Elab Term FProp
-def Differentiable.fpropExt : FPropExt where
-  fpropName := ``Differentiable
-  getFPropFun? e := 
-    if e.isAppOf ``Differentiable then
-
-      if let .some f := e.getArg? 8 then
-        some f
-      else 
-        none
-    else
-      none
-
-  replaceFTransFun e f := 
-    if e.isAppOf ``Differentiable then
-      e.modifyArg (fun _ => f) 8 
-    else          
-      e
-
-  identityRule    e :=
-    let thm : SimpTheorem :=
-    {
-      proof  := mkConst ``Differentiable.id_rule 
-      origin := .decl ``Differentiable.id_rule 
-      rfl    := false
-    }
-    FProp.tryTheorem? e thm (fun _ => pure none)
-
-  constantRule    e :=
-    let thm : SimpTheorem :=
-    {
-      proof  := mkConst ``Differentiable.const_rule 
-      origin := .decl ``Differentiable.const_rule 
-      rfl    := false
-    }
-    FProp.tryTheorem? e thm (fun _ => pure none)
-
-  lambdaLetRule    e := 
-    let thm : SimpTheorem :=
-    {
-      proof  := mkConst ``Differentiable.let_rule 
-      origin := .decl ``Differentiable.let_rule 
-      rfl    := false
-    }
-    FProp.tryTheorem? e thm (fun _ => pure none)
-
-  lambdaLambdaRule e :=
-    let thm : SimpTheorem :=
-    {
-      proof  := mkConst ``Differentiable.pi_rule 
-      origin := .decl ``Differentiable.pi_rule 
-      rfl    := false
-    }
-    FProp.tryTheorem? e thm (fun _ => pure none)
-
-  discharger e := return none
-
-
--- register fderiv
-#eval show Lean.CoreM Unit from do
-  modifyEnv (λ env => FProp.fpropExt.addEntry env (``Differentiable, Differentiable.fpropExt))
-
-
-@[fprop_rule]
-theorem HAdd.hAdd.arg_a4a5.Differentiable_comp'
-  (R : Type _) [NontriviallyNormedField R]
-  {X : Type _} [NormedAddCommGroup X] [NormedSpace R X]
-  {Y : Type _} [NormedAddCommGroup Y] [NormedSpace R Y]
-  (f g : X → Y) (hf : Differentiable R f) (hg : Differentiable R g)
-  : Differentiable R fun x => f x + g x
-  := fun x => HAdd.hAdd.arg_a4a5.DifferentiableAt_comp x f g (hf x) (hg x)
-
-
+set_option profiler.threshold 10 true
 
 example : Differentiable ℝ (fun x : ℝ => x) := by fprop
 
@@ -98,7 +14,7 @@ example : Differentiable ℝ (fun x : ℝ => x + x) := by fprop
 
 example : Differentiable ℝ (fun x : ℝ => x + x + x + x) := by fprop
 
-theorem a : 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 + 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) := 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 fprop
 
 example (x : ℝ) : Differentiable ℝ (HAdd.hAdd x) := by fprop
 
@@ -107,22 +23,22 @@ example (f : ℝ → ℝ) (hf : Differentiable ℝ f) : Differentiable ℝ (fun
 example (f : ℝ → ℝ) (hf : Differentiable ℝ f) : Differentiable ℝ (fun x => f x) := by fprop
 example (f : ℝ → ℝ) (hf : Differentiable ℝ f) : Differentiable ℝ (fun x => f x + x) := by fprop
 example (f : ℝ → ℝ) (hf : Differentiable ℝ f) : Differentiable ℝ (fun x => f x + f x) := by fprop
+example (f : ℝ → ℝ) (hf : Differentiable ℝ f) : Differentiable ℝ (fun x => f (f x)) := by fprop
 
 -- set_option trace.Meta.Tactic.fprop.step true
-
-example (f : ℝ → ℝ) (hf : Differentiable ℝ f) : Differentiable ℝ (fun x => f (f x)) := by (try fprop); sorry
-
-
 -- set_option trace.Meta.Tactic.fprop.unify true
 -- set_option trace.Meta.Tactic.fprop.apply true
--- set_option trace.Meta.Tactic.fprop.discharge true
-
+-- set_option trace.Meta.Tactic.fprop.discharge true 
 
 example (op : ℝ → ℝ → ℝ) (hop : Differentiable ℝ (fun (x,y) => op x y)) 
   (f : ℝ → ℝ) (hf : Differentiable ℝ f)
   (g : ℝ → ℝ) (hg : Differentiable ℝ g)
-  : Differentiable ℝ (fun x => op (f x) (g x)) := by (try fprop); sorry
+  : Differentiable ℝ (fun x => op (f x) (g x)) := by fprop
 
+example (op : ℝ → ℝ → ℝ) (hop : Differentiable ℝ (fun (x,y) => op x y)) 
+  (f : ℝ → ℝ) (hf : Differentiable ℝ f)
+  (g : ℝ → ℝ) (hg : Differentiable ℝ g)
+  : Differentiable ℝ (fun x => op (f x) (op (f x) (g x))) := by fprop
 
 example 
   (g : ℝ → ℝ) (hg : Differentiable ℝ g)
@@ -149,33 +65,86 @@ theorem b [Fintype ι] (f : ℝ → ι → ℝ) (hf : ∀ i, Differentiable ℝ
   : ∀ i, Differentiable ℝ (fun x => f x i) := by fprop
 
 
-@[fprop_rule]
-theorem Prod.fst.arg_self.Differentiable_comp'
-  (R : Type _) [NontriviallyNormedField R]
-  {X : Type _} [NormedAddCommGroup X] [NormedSpace R X]
-  {Y : Type _} [NormedAddCommGroup Y] [NormedSpace R Y]
-  {Z : Type _} [NormedAddCommGroup Z] [NormedSpace R Z]
-  (f : X → Y×Z) (hf : Differentiable R f)
-  : Differentiable R (fun x => (f x).1)
-  := Differentiable.fst hf
-
+example : Differentiable ℝ (fun x : ℝ => let y := x + x; y) := by fprop
 
-@[fprop_rule]
-theorem Prod.snd.arg_self.Differentiable_comp'
-  (R : Type _) [NontriviallyNormedField R]
-  {X : Type _} [NormedAddCommGroup X] [NormedSpace R X]
-  {Y : Type _} [NormedAddCommGroup Y] [NormedSpace R Y]
-  {Z : Type _} [NormedAddCommGroup Z] [NormedSpace R Z]
-  (f : X → Y×Z) (hf : Differentiable R f)
-  : Differentiable R (fun x => (f x).2)
-  := Differentiable.snd hf
+-- set_option trace.Meta.Tactic.fprop.apply true in
+-- set_option trace.Meta.Tactic.fprop.step true in
+-- set_option trace.Meta.Tactic.fprop.discharge true in
+-- set_option pp.funBinderTypes true in
+example : Differentiable ℝ (fun x : ℝ => let y := x; x) := by fprop
+
+example : Differentiable ℝ (fun x : ℝ => 
+  let x1 := x
+  let x2 := x1
+  let x3 := x2
+  x) := by fprop
+
+example : Differentiable ℝ (fun x : ℝ => 
+  let x1 := x
+  let x2 := x1
+  let x3 := x2
+  x3) := by fprop
+
+example : Differentiable ℝ (fun x : ℝ => 
+  let x1 := x
+  let x2 := x1
+  let x3 := x2
+  let x4 := x3
+  x4) := by fprop
+
+example : Differentiable ℝ (fun x : ℝ => 
+  let x1 := x
+  let x2 := x1
+  let x3 := x2
+  let x4 := x3
+  x4) := by fprop
+
+
+example : Differentiable ℝ (fun x : ℝ => 
+  let x1 := x
+  let x2 := x + x1
+  let x3 := x + x1 + x2
+  let x4 := x + x1 + x2 + x3
+  x4) := by fprop
+
+
+example : Differentiable ℝ (fun x : ℝ => 
+  let x1 := x
+  let x2 := x + x1
+  let x3 := x + x1 + x2
+  let x4 := x + x1 + x2 + x3
+  let x5 := x + x1 + x2 + x3 + x4
+  let x6 := x + x1 + x2 + x3 + x4 + x5
+  let x7 := x + x1 + x2 + x3 + x4 + x5 + x6
+  x7) := by fprop
+
+
+example : Differentiable ℝ (fun x : ℝ => 
+  let x1 := x + x
+  let x2 := x1 + x1
+  let x3 := x2 + x2
+  let x4 := x3 + x3
+  let x5 := x4 + x4
+  let x6 := x5 + x5
+  let x7 := x6 + x6
+  x7) := by fprop
+
+
+example : Differentiable ℝ (fun x : ℝ => 
+  let x1 := x
+  let x2 := x + x1
+  let x3 := x + x1 + x2
+  let x4 := x + x1 + x2 + x3
+  x4) := by fprop
 
 
-example : Differentiable ℝ (fun x : ℝ => let y := x + x; y) := by fprop
+theorem hoho : Differentiable ℝ (fun x : ℝ => let y := 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 + 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 + 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 + 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); y + 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+ x + x + x + x + x + x + x) := by fprop
 
 
-theorem hoho : Differentiable ℝ (fun x : ℝ => let y := 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 + 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 + 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 + 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); y + 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+ 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 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/FunctionSpaces/Differentiable/Test.lean b/SciLean/FunctionSpaces/Differentiable/Test.lean
index 3b2abfbc..14d90607 100644
--- a/SciLean/FunctionSpaces/Differentiable/Test.lean
+++ b/SciLean/FunctionSpaces/Differentiable/Test.lean
@@ -1,3 +1,6 @@
+import SciLean.Tactic.FProp.Basic
+import SciLean.Tactic.FProp.Notation
+
 import SciLean.FunctionSpaces.Differentiable.Basic
 
 
@@ -14,35 +17,28 @@ variable
   {E : ι → Type _} [∀ i, NormedAddCommGroup (E i)] [∀ i, NormedSpace R (E i)]
 
 
--- TODO: fix this!!!
 example
   (f : X → Y×Z) (hf : Differentiable R f)
   : Differentiable R (fun x => (f x).1)
-  := by (try differentiable); sorry
+  := by fprop
 
--- TODO: fix this!!!
 example : 
   Differentiable R (@Prod.fst X Y)
-:= by (try differentiable); sorry
+:= by fprop
 
--- TODO: fix this!!!
 example
   (f : X → Y×Z) (hf : Differentiable R f)
   : Differentiable R (fun x => (f x).2)
-  := by (try differentiable); sorry
+  := by fprop
 
--- TODO: fix this!!!
 example : 
   Differentiable R (@Prod.snd X Y)
-:= by (try differentiable); sorry
-
+:= by fprop
 
--- TODO: fix this!!!
 example
   (x' : X)
   : Differentiable R fun x : X => x' + x
-  := by (try differentiable); sorry
-
+  := by fprop
 
 
 example
@@ -70,3 +66,4 @@ example
   (hf : DifferentiableAt R f x) (hx : k ≠ 0)
   : DifferentiableAt R (fun x => f x / k) x 
   := by differentiable
+
diff --git a/SciLean/Lean/Meta/Basic.lean b/SciLean/Lean/Meta/Basic.lean
index 8cd45a44..471f374e 100644
--- a/SciLean/Lean/Meta/Basic.lean
+++ b/SciLean/Lean/Meta/Basic.lean
@@ -154,8 +154,8 @@ def mkUncurryFun (n : Nat) (f : Expr) : MetaM Expr := do
   forallTelescope (← inferType f) λ xs _ => do
     let xs := xs[0:n]
 
-    let xProdName : Name ← xs.foldlM (init:="") λ n x => 
-      do return (n.append (← x.fvarId!.getUserName).eraseMacroScopes)
+    let xProdName : String ← xs.foldlM (init:="") λ n x => 
+      do return (n ++ toString (← x.fvarId!.getUserName).eraseMacroScopes)
     let xProdType ← inferType (← mkProdElem xs)
 
     withLocalDecl xProdName default xProdType λ xProd => do
diff --git a/SciLean/Tactic/FProp/Basic.lean b/SciLean/Tactic/FProp/Basic.lean
index 0b3ead7c..3afb9a62 100644
--- a/SciLean/Tactic/FProp/Basic.lean
+++ b/SciLean/Tactic/FProp/Basic.lean
@@ -4,6 +4,49 @@ open Lean Meta Qq
 
 namespace SciLean.FProp
 
+/-- Takes lambda function `fun x => b` and splits it into composition of two functions. 
+
+  Example:
+    fun x => f (g x)      ==>   f ∘ g 
+    fun x => f x + c      ==>   (fun y => y + c) ∘ f
+    fun x => f x + g x    ==>   (fun (y₁,y₂) => y₁ + y₂) ∘ (fun x => (f x, g x))
+ -/
+def splitLambdaToComp (e : Expr) : MetaM (Expr × Expr) := do
+  match e with 
+  | .lam name type b bi => 
+    withLocalDecl name bi type fun x => do
+      let b := b.instantiate1 x
+      let xId := x.fvarId!
+
+      let ys := b.getAppArgs
+      let mut f := b.getAppFn
+
+      let mut lctx ← getLCtx
+      let instances ← getLocalInstances
+
+      let mut ys' : Array Expr := #[]
+      let mut zs  : Array Expr := #[]
+
+      for y in ys, i in [0:ys.size] do
+        if y.containsFVar xId then
+          let zId ← withLCtx lctx instances mkFreshFVarId
+          lctx := lctx.mkLocalDecl zId (name.appendAfter (toString i)) (← inferType y)
+          let z := Expr.fvar zId
+          zs  := zs.push z
+          ys' := ys'.push y
+          f := f.app z
+        else
+          f := f.app y
+
+      let y' ← mkProdElem ys'
+      let g  ← mkLambdaFVars #[.fvar xId] y'
+
+      f ← withLCtx lctx instances (mkLambdaFVars zs f)
+      f ← mkUncurryFun zs.size f
+
+      return (f, g)
+    
+  | _ => throwError "Error in `splitLambdaToComp`, not a lambda function!"
 
 def cache (e : Expr) (proof? : Option Expr) : FPropM (Option Expr) := -- return proof?
   match proof? with
@@ -13,8 +56,6 @@ def cache (e : Expr) (proof? : Option Expr) : FPropM (Option Expr) := -- return
     return proof
 
 
-
-
 def getLocalRules (fpropName : Name) : MetaM (Array SimpTheorem) := do
   let mut arr : Array SimpTheorem := #[]
 
@@ -41,7 +82,6 @@ mutual
   partial def fprop (e : Expr) : FPropM (Option Expr) := do
 
     if let .some proof := (← get).cache.find? e then
-      trace[Meta.Tactic.fprop.step] "cached\n{e}"
       return proof
     else
       forallTelescope e fun xs b => do
@@ -52,34 +92,45 @@ mutual
 
   partial def main (e : Expr) : FPropM (Option Expr) := do
 
-    -- move all leading binders into the local context
-
     let .some (fpropName, ext, f) ← getFProp? e
-      | -- not function property
-        return none
+      | return none
 
     match f with
     | .letE .. => letTelescope f fun xs b => do 
       trace[Meta.Tactic.fprop.step] "case let x := ..; ..\n{← ppExpr e}"
-      let e' := ext.replaceFTransFun e b
+      let e' := ext.replaceFPropFun e b
       fprop (← mkLambdaFVars xs e')
 
     | .lam _ _ (.bvar  0) _ => 
       trace[Meta.Tactic.fprop.step] "case id\n{← ppExpr e}"
-      applyIdentityRule ext e
+      ext.identityRule e
 
-    | .lam _ _ (.letE ..) _ => 
-      trace[Meta.Tactic.fprop.step] "case let\n{← ppExpr e}"
-      applyLambdaLetRule ext e
+    | .lam xName xType (.letE yName yType yValue body _) xBi => 
+      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 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 g := Expr.lam xName xType yValue default
+        ext.compRule e f g
+
+      | false, _ => 
+        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}"
-      applyLambdaLambdaRule ext e
+      ext.lambdaLambdaRule e f
 
     | .lam _ _ b _ => do
       if !(b.hasLooseBVar 0) then
         trace[Meta.Tactic.fprop.step] "case const\n{← ppExpr e}"
-        applyConstantRule ext e
+        ext.constantRule e
       else if b.getAppFn.isFVar then
         trace[Meta.Tactic.fprop.step] "case fvar app\n{← ppExpr e}"
         applyFVarApp e ext.discharger
@@ -90,42 +141,29 @@ mutual
     | _ => do
       trace[Meta.Tactic.fprop.step] "case other\n{← ppExpr e}"
       applyTheorems e (ext.discharger)
-  where
-    applyIdentityRule (ext : FPropExt) (e : Expr) : FPropM (Option Expr) := do
-      ext.identityRule e
-
-    applyConstantRule (ext : FPropExt) (e : Expr) : FPropM (Option Expr) := do
-      ext.constantRule e
-
-    applyLambdaLetRule (ext : FPropExt) (e : Expr) : FPropM (Option Expr) := do
-      ext.lambdaLetRule e
-
-    applyLambdaLambdaRule (ext : FPropExt) (e : Expr) : FPropM (Option Expr) := do
-      ext.lambdaLambdaRule e
 
   partial def applyFVarApp (e : Expr) (discharge? : Expr → FPropM (Option Expr)) : FPropM (Option Expr) := do
-    let .some (fpropName, _, F) ← getFProp? e
+    let .some (fpropName, ext, F) ← getFProp? e
       | return none
 
-    lambdaTelescope F fun xs b => do
-      if xs.size != 1 then 
-        panic! "invalid use of applyFVarApp! should be used only on fun x => (.fvar ..) y₁ .. yₙ"
-      let x := xs[0]!
-
-      let ys := b.getAppArgs
-      let f ← mkUncurryFun ys.size b.getAppFn
+    if ¬F.isLambda then
+      applyTheorems e discharge?
+    else
+      let (f, g) ← splitLambdaToComp F
 
-      -- trivial case
+      -- trivial case and prevent infinite loop
       if (← isDefEq f F) then
+        trace[Meta.Tactic.fprop.step] "fvar app case: trivial"
+
         applyTheorems e discharge?
       else
 
-        let g ← mkLambdaFVars #[x] (← mkProdElem ys) 
+        trace[Meta.Tactic.fprop.step] "fvar app case: decomposed into `({← ppExpr f}) ∘ ({← ppExpr g})`"
 
-        trace[Meta.Tactic.fprop.step] "composition case\n`{← ppExpr f} ∘ {← ppExpr g}`"
+        let fg ← mkAppM ``Function.comp #[f,g]
+        let e' := ext.replaceFPropFun e fg
         
-        return none
-
+        fprop e' -- are we abusing `Function.comp` defeq here?
 
   partial def applyTheorems (e : Expr) (discharge? : Expr → FPropM (Option Expr)) : FPropM (Option Expr) := do
     let .some (fpropName, ext, f) ← getFProp? e
@@ -138,15 +176,18 @@ mutual
         | .some funName => FProp.getFPropRules funName fpropName
         | none => getLocalRules fpropName
 
+    if candidates.size = 0 then
+      trace[Meta.Tactic.fprop.apply] "no suitable theorems found for {← ppExpr e}"
+
     for thm in candidates do
+      trace[Meta.Tactic.fprop.unify] "trying to apply {← ppOrigin thm.origin} to {← ppExpr e}"
       if let some proof ← tryTheorem? e thm discharge? then
         return proof
 
-    ext.lambdaLetRule e
+    return none -- ext.lambdaLetRule e
     -- return none
 
-
-  partial def synthesizeInstance (thmId : Origin) (x type : Expr) : MetaM Bool := do 
+  partial def synthesizeInstance (thmId : Origin) (x type : Expr) : MetaM Bool := do
     match (← trySynthInstance type) with
     | LOption.some val =>
       if (← withReducibleAndInstances <| isDefEq x val) then
diff --git a/SciLean/Tactic/FProp/Init.lean b/SciLean/Tactic/FProp/Init.lean
index 819c1f7c..51e92ab8 100644
--- a/SciLean/Tactic/FProp/Init.lean
+++ b/SciLean/Tactic/FProp/Init.lean
@@ -45,17 +45,19 @@ structure _root_.SciLean.FPropExt where
   /-- Function transformation name -/
   fpropName : Name
   /-- Get the function  -/
-  getFPropFun?    (expr : Expr) : Option Expr
+  getFPropFun?     (expr : Expr) : Option Expr
   /-- Replace the function -/
-  replaceFTransFun (expr : Expr) (newFun : Expr) : Expr
+  replaceFPropFun  (expr : Expr) (newFun : Expr) : Expr
   /-- Custom rule for proving property of `fun x => x -/
   identityRule     (expr : Expr) : FPropM (Option Expr)
   /-- Custom rule for proving property of `fun x => y -/
   constantRule     (expr : Expr) : FPropM (Option Expr)
+  /-- Custom rule for proving property of `fun x => f (g x)` or `fun x => let y := g x; f y` -/
+  compRule         (expr f g : Expr) : FPropM (Option Expr)
   /-- Custom rule for proving property of `fun x => let y := g x; f x y -/
-  lambdaLetRule    (expr : Expr) : FPropM (Option Expr)
+  lambdaLetRule    (expr f g : Expr) : FPropM (Option Expr)
   /-- Custom rule for proving property of `fun x y => f x y -/
-  lambdaLambdaRule (expr : Expr) : FPropM (Option Expr)
+  lambdaLambdaRule (expr f : Expr) : FPropM (Option Expr)
   /-- Custom discharger for this function property - like proving (x≠0) -/
   discharger       : Expr → FPropM (Option Expr)
   /-- Name of this extension, keep the default value! -/