diff --git a/checker/__init__.py b/checker/__init__.py
new file mode 100644
index 0000000..fa5d77c
--- /dev/null
+++ b/checker/__init__.py
@@ -0,0 +1,15 @@
+"""
+    This module hosts various elements that are necessary to create a proof
+    checker.
+"""
+
+from .props import And, Implies, Prop
+from .terms import Term, register_known_const
+
+__all__ = [
+    "And",
+    "Implies",
+    "Prop",
+    "Term",
+    "register_known_const",
+]
diff --git a/checker/proof.py b/checker/proof.py
new file mode 100644
index 0000000..57c9926
--- /dev/null
+++ b/checker/proof.py
@@ -0,0 +1,57 @@
+"""
+    The proofs module contains various methods to construct a proof.
+"""
+
+from __future__ import annotations
+
+import .props as p
+
+from .props import Context, Prop
+
+class ProofCheckerFailedException(Exception):
+    pass
+
+class Proof:
+    """
+        Base class to construct a proof.
+    """
+
+# -----------------------------------------------------------------------------
+
+class Reflexivity(Proof):
+    """
+        Reflectivity proof checker that solves t = t.
+    """
+
+    def __init__(self, ctx : Context, goal : Prop) -> None:
+        """
+            Create a new proof that uses reflexivity. This axiom defines that
+            variables equal oneselves.
+
+            :param ctx: The context with which one wants to prove this.
+            :type ctx: Context
+            :param goal: The equality that needs to be proven.
+            :type goal: Prop
+            :raises ProofCheckerFailedException: The proof checker cannot
+                verify the goal.
+        """
+
+        match goal:
+            case p.Eq():
+                lhs = goal.x.normalize()
+                rhs = goal.y.normalize()
+
+                if lhs == rhs:
+                    self.ctx = ctx
+                    self.goal = goal
+                else:
+                    l, r = lhs.reduce_on_equality(rhs)
+
+                    raise ProofCheckerFailedException(
+                        f"Could not prove that {lhs} = {rhs}. Got stuck on {l} = {r}."
+                    )
+            
+            case _:
+                raise ProofCheckerFailedException(
+                    "Reflexivity can only prove that t = t. Found another prop type than `Eq`."
+                )
diff --git a/checker/props.py b/checker/props.py
new file mode 100644
index 0000000..5236bec
--- /dev/null
+++ b/checker/props.py
@@ -0,0 +1,127 @@
+"""
+    This module hosts propositions.
+"""
+
+from __future__ import annotations
+
+from .terms import Term
+from dataclasses import dataclass
+
+@dataclass(frozen=True)
+class Context:
+    """
+        The Context is a collection of propositions. These are the hypotheses
+        that are used to arrive at a proof.
+    """
+    props : list["Prop"]
+
+    def with_prop(self, new_prop : "Prop") -> Context:
+        return Context(props=[ prop for prop in self.props ] + [ new_prop ])
+
+class Prop:
+    """
+        A proposition is a logical statement. It can be proven by the proof
+        checker, or it can be used as a hypothesis to prove another
+        proposition.
+    """
+
+    def as_assumption(self, goal : Prop) -> list[list[tuple[list[Prop], Prop]]]:
+        """
+            Propositions can simplify the proof by creating simpler theorems
+            and sub-lemmas to prove instead. If this proposition is part of
+            the assumptions, this function helps transform the goal into
+            simpler sub-goals.
+
+            :return: Tuples of added assumptions with a new goal.
+            :rtype: list[list[tuple[list[Prop], Prop]]]
+        """
+        return []
+
+    def as_proof(self) -> list[list[tuple[list[Prop], Prop]]]:
+        """
+            Determine which hypotheses are required in the context to prove
+            this proposition.
+
+            The function returns a list of various methods to prove the
+            proposition. If any of the methods is an empty list, it means
+            the proposition requires no assumptions and can instead be
+            computed.
+
+            :return: Methods to prove this proposition.
+            :rtype: list[tuple[list[Prop], Prop]]
+        """
+        return []
+
+@dataclass(frozen=True)
+class And(Prop):
+    """
+        The logical and-operator `P ^ Q`.
+    """
+
+    P : Prop
+    Q : Prop
+
+    def as_assumption(self, goal: Prop) -> list[list[tuple[list[Prop], Prop]]]:
+        return [
+            [ ( [ self.P, self.Q ], goal )
+            ],
+        ]
+    
+    def as_proof(self) -> list[list[tuple[list[Prop], Prop]]]:
+        return [
+            [ ( [], self.P )
+            , ( [], self.Q )
+            ],
+        ]
+
+class Eq(Prop):
+    """
+        Compare whether two terms are equal.
+    """
+
+    x : Term
+    y : Term
+
+    def as_assumption(self, goal: Prop) -> list[list[tuple[list[Prop], Prop]]]:
+        return []
+    
+    def as_proof(self) -> list[list[tuple[list[Prop], Prop]]]:
+        return super().as_proof()
+
+@dataclass(frozen=True)
+class Implies(Prop):
+    """
+        The logical operator `P -> Q`.
+    """
+
+    P : Prop
+    Q : Prop
+
+    def as_assumption(self, goal : Prop) -> list[list[tuple[list[Prop], Prop]]]:
+        return [
+            [ ( [], self.P )
+            , ( [ self.Q ], goal)
+            ],
+        ]
+    
+    def as_proof(self) -> list[list[tuple[list[Prop], Prop]]]:
+        return [
+            [ ( [ self.P ], self.Q )
+            ],
+        ]
+
+# @dataclass(frozen=True)
+# class Or(Prop):
+#     """
+#         The logical and-operator `P v Q`.
+#     """
+
+#     P : Prop
+#     Q : Prop
+
+#     def as_assumption(self, goal: Prop) -> list[list[tuple[list[Prop], Prop]]]:
+#         return [
+
+#         ]
+    
+
diff --git a/checker/terms.py b/checker/terms.py
new file mode 100644
index 0000000..482ce45
--- /dev/null
+++ b/checker/terms.py
@@ -0,0 +1,188 @@
+"""
+    Terms are values in an equation. They can be constants, variables,
+    functions, operators, and many more.
+"""
+
+from __future__ import annotations
+
+import copy
+
+from dataclasses import dataclass
+
+__known_consts : dict[str, Term] = {
+}
+
+def register_known_const(name : str, value : Term) -> None:
+    __known_consts[name] = value
+
+class Term:
+    """
+        Base class for all terms.
+    """
+    
+    def normalize(self) -> Term:
+        """
+            Function to return a simplified version of the term.
+        """
+        return self
+    
+    def reduce_on_equality(self, other : Term) -> tuple[Term, Term]:
+        """
+            Reduce parts that the two items are equal on.
+        """
+        return self, other
+    
+    def substitute(self, index : int, value : Term) -> Term:
+        """
+            Substitute all variables of a given index number.
+
+            :param index: The variable's index.
+            :type index: int
+            :param value: The value to replace the variable with.
+            :type value: 
+        """
+        return self
+
+@dataclass(frozen=True)
+class App(Term):
+    """
+        An App is the application of a function with an argument.
+        You could consider it the inverse of the lambda function.
+    """
+
+    f : Term
+    x : Term
+
+    def normalize(self) -> Term:
+        f = self.f.normalize()
+        x = self.x.normalize()
+
+        default = App(f=f, x=x)
+
+        match f:
+            case App():
+                return default
+
+            case Const():
+                return default
+
+            case Lambda():
+                return f.resolve(x)
+
+            case Term():
+                return default
+            
+            case Var():
+                return default
+    
+    def reduce_on_equality(self, other: Term) -> tuple[Term, Term]:
+        if not isinstance(other, App):
+            return self, other
+        
+        f1, f2 = self.f.normalize(), other.f.normalize()
+        x1, x2 = self.x.normalize(), other.x.normalize()
+
+        match ( f1 == f2, x1 == x2 ):
+            case ( True, True ):
+                return Term(), Term()
+            
+            case ( True, False ):
+                return x1.reduce_on_equality(x2)
+            
+            case ( False, True ):
+                return f1.reduce_on_equality(f2)
+            
+            case ( False, False ):
+                return self, other
+
+    def substitute(self, index : int, value : Term) -> Term:
+        """
+            Substitute all variables of a given index number.
+
+            :param index: The variable's index.
+            :type index: int
+            :param value: The value to replace the variable with.
+            :type value: 
+        """
+        return App(
+            f=self.f.substitute(index=index, value=value),
+            x=self.x.substitute(index=index, value=value),
+        )
+
+@dataclass(frozen=True)
+class Const(Term):
+    """
+        Constants are 0-ary functions. They can represent variables, constants
+        or other values that generally take no input.
+    """
+
+    name : str
+
+    def normalize(self) -> Term:
+        if self.name in __known_consts:
+            return copy.deepcopy(__known_consts.get(self.name, self))
+        else:
+            return self
+
+@dataclass(frozen=True)
+class Lambda(Term):
+    """
+        Lambdas a nameless 1-ary functions.
+    """
+
+    out : Term
+
+    def normalize(self) -> Term:
+        return Lambda(out=self.out.normalize())
+    
+    def reduce_on_equality(self, other: Term) -> tuple[Term, Term]:
+        match other:
+            case Lambda():
+                return self.out, other.out
+            case _:
+                return self, other
+
+    def resolve(self, value : Term) -> Term:
+        """
+            Resolve this lambda function by inserting a value.
+
+            :param value: The value to substitute.
+        """
+        return self.substitute(index=-1, value=value)
+
+    def substitute(self, index : int, value : Term) -> Term:
+        """
+            Substitute all variables of a given index number.
+
+            :param index: The variable's index.
+            :type index: int
+            :param value: The value to replace the variable with.
+            :type value: 
+        """
+        if index == -1:
+            # We're resolving this lambda function!
+            return self.out.substitute(index=index + 1, value=value)
+        else:
+            return Lambda(out=self.out.substitute(index=index + 1, value=value))
+
+@dataclass(frozen=True)
+class Var(Term):
+    """
+        A variable is a value that can be substituted by a lambda function.
+    """
+
+    index : int
+
+    def substitute(self, index : int, value : Term) -> Term:
+        """
+            Substitute all variables of a given index number.
+
+            :param index: The variable's index.
+            :type index: int
+            :param value: The value to replace the variable with.
+            :type value: 
+        """
+        if self.index == index:
+            return copy.deepcopy(value)
+        else:
+            return self
diff --git a/proof.py b/proof.py
index b3bfe22..0ad1db9 100644
--- a/proof.py
+++ b/proof.py
@@ -147,6 +147,9 @@ class Assumption(Proof):
 class Refl(Proof):
     def apply(self, goal : Prop, ctx : Context) -> Prop:
         match goal:
+            case Contradict():
+                return goal
+            
             case Eq():
                 l = normalize(goal.lhs)
                 r = normalize(goal.rhs)
@@ -171,10 +174,68 @@ class Refl(Proof):
                         f"Couldn't normalize {goal.lhs} = {goal.rhs} any further than to {l} = {r}"
                     )
             
+            case Trivial():
+                return goal
+
             case Prop():
+                return goal
+
+@dataclass(frozen=True)
+class Rewrite(Proof):
+    m : Term
+    s : Term
+
+    def apply(self, goal : Prop, ctx : Context) -> Prop:
+        if Eq(lhs=self.m, rhs=self.s) not in ctx.props:
+            if Eq(lhs=self.s, rhs=self.m) not in ctx.props:
                 return Contradict(
-                    "Cannot prove base proposition"
+                    f"Could not find justification why you would be able to substitute {self.m} with {self.s}"
                 )
+        
+        match goal:
+            case Contradict():
+                return goal
+
+            case Eq(lhs=lhs, rhs=rhs):
+                return Eq(
+                    lhs=self.find_and_replace(lhs),
+                    rhs=self.find_and_replace(rhs),
+                )
+            
+            case Prop():
+                return goal
+            
+            case Trivial():
+                return goal
+
+    def find_and_replace(self, term : Term) -> Term:
+        if term == self.m or term == self.s:
+            return self.s
+        
+        match term:
+            case App(f=f, x=x):
+                return App(
+                    f=self.find_and_replace(f),
+                    x=self.find_and_replace(x),
+                )
+        
+            case Const():
+                return term
+            
+            case Term():
+                return term
+
+@dataclass(frozen=True)
+class Script(Proof):
+    steps : list[Proof]
+
+    def apply(self, goal: Prop, ctx: Context) -> Prop:
+        state = goal
+
+        for step in self.steps:
+            state = step.apply(state, ctx)
+        
+        return state
 
 # -----------------------------------------------------------------------------
 # Context
@@ -349,3 +410,18 @@ if __name__ == "__main__":
         Refl(),
         Context(props=[]),
     ))
+
+    # x + 4 = 6 when x = 2
+    print(check(
+        goal=Eq(
+            lhs=A2("Nat.add", Const("x"), kernel_from_int(4)),
+            rhs=kernel_from_int(6),
+        ),
+        proof=Script([
+            Rewrite(m=Const("x"), s=kernel_from_int(2)),
+            Refl()
+        ]),
+        ctx=Context([
+            Eq(Const("x"), kernel_from_int(2)),
+        ]),
+    ))