diff --git a/mambo.agda b/mambo.agda
index 1c3d7d6..a4db8db 100644
--- a/mambo.agda
+++ b/mambo.agda
@@ -215,10 +215,38 @@ weak-modal (□ᵢ x) x₁ = □ᵢ (weak x x₁)
 weak-modal (□ₑ x x₂) x₁ = □ₑ (weak-modal x x₁) (weak-modal x₂ (inBoth x₁))
 
 cut : (Γ' : Context) → Δ / Γ ⊢ A → Δ / Γ' ++ (Γ , A) ⊢ B → Δ / Γ' ++ Γ ⊢ B
-cut Γ' x x₁ = {!!}
+cut [] x (var x₁) = mp (⇒ᵢ (var x₁)) x
+cut (Γ' , x₂) x (var (zero x₁ xs)) = var (zero x₂ (Γ' ++ _))
+cut (Γ' , x₂) x (var (succ _ xs x₃)) = weak (cut Γ' x (var x₃)) λ {X} → succ X (Γ' ++ _)
+cut Γ' x (mp x₁ x₂) = mp (cut Γ' x x₁) (cut Γ' x x₂)
+cut Γ' x (∧ᵢ x₁ x₂) = ∧ᵢ (cut Γ' x x₁) (cut Γ' x x₂)
+cut Γ' x (∧ₑ₁ x₁) = ∧ₑ₁ (cut Γ' x x₁)
+cut Γ' x (∧ₑ₂ x₁) = ∧ₑ₂ (cut Γ' x x₁)
+cut Γ' x (∨ᵢ₁ x₁) = ∨ᵢ₁ (cut Γ' x x₁)
+cut Γ' x (∨ᵢ₂ x₁) = ∨ᵢ₂ (cut Γ' x x₁)
+cut Γ' x (∨ₑ x₁ x₂ x₃) = ∨ₑ (cut Γ' x x₁) (cut (Γ' , _) x x₂) (cut (Γ' , _ ) x x₃)
+cut Γ' x (⇒ᵢ x₁) = ⇒ᵢ (cut (Γ' , _) x x₁)
+cut Γ' x (¬ᵢ x₁) = ¬ᵢ (cut (Γ' , _) x x₁)
+cut Γ' x (¬ₑ x₁ x₂) = ¬ₑ (cut Γ' x x₁) (cut Γ' x x₂)
+cut Γ' x (⊥ₑ x₁) = ⊥ₑ (cut Γ' x x₁)
+cut Γ' x (□ᵢ x₁) = □ᵢ x₁
+cut Γ' x (□ₑ x₁ x₂) = □ₑ (cut Γ' x x₁) (cut Γ' (weak-modal x (λ {X = X₁} → succ X₁ _)) x₂)
 
-cut-modal : Δ / Γ ⊢ A → Δ' ++ (Δ , A) / Γ ⊢ B → Δ' ++ Δ / Γ ⊢ B
-cut-modal = {!!}
+cut-modal : (Δ' : Context) → [] / Δ ⊢ A → Δ' ++ (Δ , A) / Γ ⊢ B → Δ' ++ Δ / Γ ⊢ B
+cut-modal Δ' x (var x₁) = var x₁
+cut-modal Δ' x (mp x₁ x₂) = mp (cut-modal Δ' x x₁) (cut-modal Δ' x x₂)
+cut-modal Δ' x (∧ᵢ x₁ x₂) = ∧ᵢ (cut-modal Δ' x x₁) (cut-modal Δ' x x₂)
+cut-modal Δ' x (∧ₑ₁ x₁) = ∧ₑ₁ (cut-modal Δ' x x₁)
+cut-modal Δ' x (∧ₑ₂ x₁) = ∧ₑ₂ (cut-modal Δ' x x₁)
+cut-modal Δ' x (∨ᵢ₁ x₁) = ∨ᵢ₁ (cut-modal Δ' x x₁)
+cut-modal Δ' x (∨ᵢ₂ x₁) = ∨ᵢ₂ (cut-modal Δ' x x₁)
+cut-modal Δ' x (∨ₑ x₁ x₂ x₃) = ∨ₑ (cut-modal Δ' x x₁) (cut-modal Δ' x x₂) (cut-modal Δ' x x₃)
+cut-modal Δ' x (⇒ᵢ x₁) = ⇒ᵢ (cut-modal Δ' x x₁)
+cut-modal Δ' x (¬ᵢ x₁) = ¬ᵢ (cut-modal Δ' x x₁)
+cut-modal Δ' x (¬ₑ x₁ x₂) = ¬ₑ (cut-modal Δ' x x₁) (cut-modal Δ' x x₂)
+cut-modal Δ' x (⊥ₑ x₁) = ⊥ₑ (cut-modal Δ' x x₁)
+cut-modal Δ' x (□ᵢ x₁) = □ᵢ (cut Δ' x x₁)
+cut-modal Δ' x (□ₑ x₁ x₂) = □ₑ (cut-modal Δ' x x₁) (cut-modal (Δ' , _) x x₂)
 
 KSym : [] / [] ⊢ □ (X ⇒ Y) ⇒ (□ X ⇒ □ Y)
 KSym {X} {Y} = ⇒ᵢ (⇒ᵢ (□ₑ (var (zero (□ X) ([] , (□ (X ⇒ Y)))))