diff --git a/logic/proof.py b/logic/proof.py
index 7ed1ceb..c6854c5 100644
--- a/logic/proof.py
+++ b/logic/proof.py
@@ -1,9 +1,17 @@
-from typing import Sequence, Generator, Iterator, TypeAlias
-from .proposition import *
+from typing import Sequence, Generator, Iterator, TypeAlias, Any
+from .proposition import (
+    Statement,
+    CompositePropositionAND,
+    CompositePropositionNOT,
+    CompositePropositionOR,
+    CompositePropositionBICONDITIONAL,
+    CompositePropositionCONDITIONAL,
+)
 
 from enum import Enum
 
 AssumptionT: TypeAlias = "Assumption"
+ProofT: TypeAlias = "Proof"
 
 
 class RulesOfInference(Enum):
@@ -21,7 +29,7 @@ class RulesOfInference(Enum):
 
 
 class Assumption:
-    def __init__(self, assumptions: Sequence[Statement] | Self) -> None:
+    def __init__(self, assumptions: Sequence[Statement] | AssumptionT) -> None:
         if isinstance(assumptions, Assumption):
             self.assumptions: set[Statement] = set(assumptions.assumptions)
         else:
@@ -31,10 +39,10 @@ def __contains__(self, key: Any) -> bool:
         return key in self.assumptions
 
     def with_proposition(self, prop: Statement) -> Generator[Statement, None, None]:
-        l = prop.extract()
+        individual_propositions = prop.extract()
         for i in self.assumptions:
             yielded = False
-            for j in l:
+            for j in individual_propositions:
                 if j in i and not yielded:
                     yielded = True
                     yield i
@@ -56,7 +64,7 @@ def __init__(self) -> None:
     def add(self, roi: RulesOfInference, *statement: Statement) -> None:
         self.proof.append((roi, (*statement,)))
 
-    def extend(self, proof: Self) -> None:
+    def extend(self, proof: ProofT) -> None:
         self.proof.extend(proof.proof)
 
     def __iter__(self) -> Iterator[tuple[RulesOfInference, tuple[Statement, ...]]]:
@@ -244,7 +252,7 @@ def prove(self) -> tuple[Proof, bool]:
                             self.proof.add(RulesOfInference.Resolution, i)
                             self.proof.extend(proof)
                             return self.proof, True
-                        
+
                     # Applying Disjunctive Syllogism
                     if self.conclusion == first:
                         proof, truth = Prover(self.assumptions.remove(i), ~second).prove()
diff --git a/logic/proposition.py b/logic/proposition.py
index 6aa76c0..6579094 100644
--- a/logic/proposition.py
+++ b/logic/proposition.py
@@ -1,4 +1,4 @@
-from typing import Self, Any, TypeAlias
+from typing import Any, TypeAlias
 from copy import copy
 from abc import ABC, abstractmethod
 from warnings import warn
@@ -27,27 +27,27 @@ def extract(self) -> list[PropositionT]:
     def __contains__(self, key: Any) -> bool:
         pass
 
-    def __and__(self, other: Any) -> CompositePropositionT:
+    def __and__(self, other: Any) -> StatementT:
         if not isinstance(other, Statement):
             raise TypeError(f"Cannot perform logical and of {type(self)} with {type(other)}")
         return CompositePropositionAND(self, other)
 
-    def __or__(self, other: Any) -> CompositePropositionT:
+    def __or__(self, other: Any) -> StatementT:
         if not isinstance(other, Statement):
             raise TypeError(f"Cannot perform logical or of {type(self)} with {type(other)}")
         return CompositePropositionOR(self, other)
 
-    def __invert__(self) -> CompositePropositionT:
+    def __invert__(self) -> StatementT:
         if isinstance(self, CompositePropositionNOT):
             return copy(self.statement)
         return CompositePropositionNOT(self)
 
-    def __truediv__(self, other: Any) -> CompositePropositionT:
+    def __truediv__(self, other: Any) -> StatementT:
         if not isinstance(other, Statement):
             raise TypeError(f"Cannot perform logical imply of {type(self)} with {type(other)}")
         return CompositePropositionCONDITIONAL(self, other)
 
-    def __mod__(self, other: Any) -> CompositePropositionT:
+    def __mod__(self, other: Any) -> StatementT:
         if not isinstance(other, Statement):
             raise TypeError(f"Cannot perform logical bi-conditional of {type(self)} with {type(other)}")
         return CompositePropositionBICONDITIONAL(self, other)