diff --git a/src/main/scala/com/melvic/chi/Evaluate.scala b/src/main/scala/com/melvic/chi/Evaluate.scala
index 555150c..c52d1bb 100644
--- a/src/main/scala/com/melvic/chi/Evaluate.scala
+++ b/src/main/scala/com/melvic/chi/Evaluate.scala
@@ -6,25 +6,14 @@ import com.melvic.chi.ast.Proposition._
 import com.melvic.chi.ast.{Definition, Proof, Proposition, Signature}
 import com.melvic.chi.env.Environment
 import com.melvic.chi.env.Environment.Environment
+import com.melvic.chi.env.implicits._
 
 object Evaluate {
   //noinspection SpellCheckingInspection
   def proposition(proposition: Proposition)(implicit env: Environment): Result[Proof] =
     proposition match {
       case PUnit => Result.success(TUnit)
-      case atom: Atom =>
-        Environment
-          .findAtom(atom)
-          .toRight(Fault.cannotProve(atom))
-          .flatMap {
-            case variable @ Variable(name, `atom`) => Result.success(variable)
-            case variable @ Variable(f, Implication(antecedent, _)) =>
-              Evaluate.proposition(antecedent)(env.filterNot(_ == variable)).map {
-                case TUnit                    => Application(f, Nil)
-                case Proof.Conjunction(terms) => Application(f, terms)
-                case param                    => Application(f, List(param))
-              }
-          }
+      case atom: Atom => applyAssumptionRule(atom)
       case Conjunction(components) => conjunctionIntroduction(components)
       case Disjunction(left, right) =>
         Evaluate
@@ -74,4 +63,22 @@ object Evaluate {
     val evaluatedComponents = recurse(Nil, components)
     evaluatedComponents.map(Proof.Conjunction)
   }
+
+  def applyAssumptionRule(atom: Atom)(implicit env: Environment): Result[Proof] =
+    Environment
+      .findAtom(atom)(env)
+      .toRight(Fault.cannotProve(atom))
+      .flatMap {
+        case variable @ Variable(name, `atom`) => Result.success(variable)
+        case variable @ Variable(f, Implication(antecedent, _)) =>
+          val newEnv: Environment = env.discharge(variable)
+          Evaluate
+            .proposition(antecedent)(newEnv)
+            .map {
+              case TUnit                    => Application(f, Nil)
+              case Proof.Conjunction(terms) => Application(f, terms)
+              case param                    => Application(f, List(param))
+            }
+            .orElse(applyAssumptionRule(atom)(newEnv))
+      }
 }
diff --git a/src/main/scala/com/melvic/chi/env/Environment.scala b/src/main/scala/com/melvic/chi/env/Environment.scala
index 6c7d05a..22d9181 100644
--- a/src/main/scala/com/melvic/chi/env/Environment.scala
+++ b/src/main/scala/com/melvic/chi/env/Environment.scala
@@ -22,6 +22,9 @@ object Environment {
       case _                                   => false
     }
 
+  def discharge(env: Environment, proof: Proof): Environment =
+    env.filterNot(_ == proof)
+
   /**
     * Assigns a variable to the proposition and registers it into the environment
     */
diff --git a/src/main/scala/com/melvic/chi/env/implicits.scala b/src/main/scala/com/melvic/chi/env/implicits.scala
new file mode 100644
index 0000000..1ecf773
--- /dev/null
+++ b/src/main/scala/com/melvic/chi/env/implicits.scala
@@ -0,0 +1,11 @@
+package com.melvic.chi.env
+
+import com.melvic.chi.ast.Proof
+import com.melvic.chi.env.Environment.Environment
+
+object implicits {
+  implicit class EnvironmentOps(env: Environment) {
+    def discharge(proof: Proof): Environment =
+      Environment.discharge(env, proof)
+  }
+}
diff --git a/src/test/scala/com/melvic/chi/tests/ScalaDefSpec.scala b/src/test/scala/com/melvic/chi/tests/ScalaDefSpec.scala
index dc248ca..0c942ee 100644
--- a/src/test/scala/com/melvic/chi/tests/ScalaDefSpec.scala
+++ b/src/test/scala/com/melvic/chi/tests/ScalaDefSpec.scala
@@ -77,6 +77,18 @@ class ScalaDefSpec extends AnyFlatSpec with should.Matchers {
     )
   }
 
+  "all assumptions" should "be considered" in {
+    generateAndShow("def foo[A, B, C]: (A => C) => (B => C) => B => C") should be(
+      """def foo[A, B, C]: ((A => C) => ((B => C) => (B => C))) =
+        |  f => g => b => g(b)""".stripMargin
+    )
+
+    generateAndShow("def foo[A, B, C]: (B => C) => (A => C) => B => C") should be(
+      """def foo[A, B, C]: ((B => C) => ((A => C) => (B => C))) =
+        |  f => g => b => f(b)""".stripMargin
+    )
+  }
+
   "Unknown propositions" should "not be allowed" in {
     generateAndShow("def foo[A]: A => B") should be(
       "Unknown propositions: B"