diff --git a/.gitignore b/.gitignore
index bfb30ec..7b6d52e 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1 +1,3 @@
 /.lake
+
+*.png
\ No newline at end of file
diff --git a/LabelledSystem.lean b/LabelledSystem.lean
index 7acb209..aa6919f 100644
--- a/LabelledSystem.lean
+++ b/LabelledSystem.lean
@@ -1,5 +1,2 @@
-import LabelledSystem.Basic
-
-import LabelledSystem.Gentzen.Basic
 import LabelledSystem.Gentzen.Soundness
-import LabelledSystem.Gentzen.Hilbert
+import LabelledSystem.Gentzen.Completeness
diff --git a/LabelledSystem/Gentzen/Cut.lean b/LabelledSystem/Gentzen/Cut.lean
index 1071178..d741c63 100644
--- a/LabelledSystem/Gentzen/Cut.lean
+++ b/LabelledSystem/Gentzen/Cut.lean
@@ -3,6 +3,7 @@ import LabelledSystem.Gentzen.Contraction
 namespace LO.Modal.Labelled.Gentzen
 
 variable {S₁ S₂ : Sequent}
+variable {Φ₁ Φ₂ Ψ₁ Ψ₂ : LabelledFormulae} {X₁ X₂ Y₁ Y₂ : RelTerms}
 
 noncomputable def cutRel
   (d₁ : ⊢ᵍ S₁.Γ ⟹ ⟨S₁.Δ.fmls, (x, y) ::ₘ S₁.Δ.rels⟩)
@@ -18,4 +19,10 @@ noncomputable def cutFml
   induction c with
   | _ => sorry;
 
+noncomputable def cutFmlₐ (x φ)
+  (d₁ : ⊢ᵍ ⟨Φ₁, X₁⟩ ⟹ ⟨(x ∶ φ) ::ₘ Ψ₁, Y₁⟩)
+  (d₂ : ⊢ᵍ ⟨(x ∶ φ) ::ₘ Φ₂, X₂⟩ ⟹ ⟨Ψ₂, Y₂⟩)
+  : ⊢ᵍ (⟨Φ₁ + Φ₂, X₁ + X₂⟩) ⟹ (⟨Ψ₁ + Ψ₂, Y₁ + Y₂⟩) := by
+  refine @cutFml (S₁ := ⟨Φ₁, X₁⟩ ⟹ ⟨Ψ₁, Y₁⟩) (S₂ := ⟨Φ₂, X₂⟩ ⟹ ⟨Ψ₂, Y₂⟩) x φ d₁ d₂;
+
 end LO.Modal.Labelled.Gentzen
diff --git a/LabelledSystem/Gentzen/Hilbert.lean b/LabelledSystem/Gentzen/Hilbert.lean
index 81d294d..e7794c9 100644
--- a/LabelledSystem/Gentzen/Hilbert.lean
+++ b/LabelledSystem/Gentzen/Hilbert.lean
@@ -1,5 +1,3 @@
-import LabelledSystem.Gentzen.Weakening
-import LabelledSystem.Gentzen.Inverted
 import LabelledSystem.Gentzen.Cut
 
 namespace LO.Modal
@@ -52,8 +50,7 @@ def axiomK : ⊢ᵍ ↑(□(φ ➝ ψ) ➝ □φ ➝ □ψ) := by
   . exact initFml_mem 1 φ (by simp) (by simp);
   . exact initFml_mem 1 ψ (by simp) (by simp);
 
-def mdp (d₁ : ⊢ᵍ ↑(φ ➝ ψ)) (d₂ : ⊢ᵍ ↑φ) : ⊢ᵍ ↑ψ := by
-  simpa using cutFml (Δ₁ := ⟨∅, ∅⟩) (Δ₂ := ⟨{_ ∶ ψ}, ∅⟩) d₂ $ implyRInv (Δ := ⟨∅, ∅⟩) d₁;
+noncomputable def mdp (d₁ : ⊢ᵍ ↑(φ ➝ ψ)) (d₂ : ⊢ᵍ ↑φ) : ⊢ᵍ ↑ψ := cutFmlₐ 0 φ d₂ (implyRInvₐ d₁)
 
 noncomputable def necessitation (d : ⊢ᵍ ↑φ) : ⊢ᵍ ↑(□φ) := by
   apply boxRₐ 0 1 φ (by simp) (by simp [isFreshLabel]) (by simp [isFreshLabel]);
diff --git a/LabelledSystem/Gentzen/Inverted.lean b/LabelledSystem/Gentzen/Inverted.lean
index 888bba9..5aba138 100644
--- a/LabelledSystem/Gentzen/Inverted.lean
+++ b/LabelledSystem/Gentzen/Inverted.lean
@@ -14,6 +14,11 @@ def implyRInv
   : ⊢ᵍ (⟨(x ∶ φ) ::ₘ S.Γ.fmls, S.Γ.rels⟩ ⟹ ⟨(x ∶ ψ) ::ₘ S.Δ.fmls, S.Δ.rels⟩)
   := implyRInvₕ (d := .ofDerivation d) |>.drv
 
+def implyRInvₐ
+  (d : ⊢ᵍ (⟨Φ, X⟩ ⟹ ⟨(x ∶ φ ➝ ψ) ::ₘ Ψ, Y⟩))
+  : ⊢ᵍ (⟨(x ∶ φ) ::ₘ Φ, X⟩ ⟹ ⟨(x ∶ ψ) ::ₘ Ψ, Y⟩)
+  := implyRInv (S := ⟨Φ, X⟩ ⟹ ⟨Ψ, Y⟩) d
+
 
 def implyLInv₁ₕ
   (d : ⊢ᵍ[h] (⟨(x ∶ φ ➝ ψ) ::ₘ S.Γ.fmls, S.Γ.rels⟩ ⟹ S.Δ))