diff --git a/mambo.agda b/mambo.agda
index 8d44fc6..9bedd73 100644
--- a/mambo.agda
+++ b/mambo.agda
@@ -185,20 +185,20 @@ inBoth {A} {Γ} {Γ'} {X} x {X₁} (zero x₁ xs) = zero X Γ'
 inBoth {A} {Γ} {Γ'} {X} x {X₁} (succ x₁ xs x₂) = succ X₁ Γ' (x x₂)
 
 weak : Δ / Γ ⊢ A → Γ ⊆ Γ' → Δ / Γ' ⊢ A
-weak {Δ} {Γ} {A} {Γ'} (var x) x₁ = var (x₁ x)
-weak {Δ} {Γ} {A} {Γ'} (mp x x₂) x₁ = mp (weak x x₁) (weak x₂ x₁)
-weak {Δ} {Γ} {A} {Γ'} (∧ᵢ x x₂) x₁ = ∧ᵢ (weak x x₁) (weak x₂ x₁)
-weak {Δ} {Γ} {A} {Γ'} (∧ₑ₁ x) x₁ = ∧ₑ₁ (weak x x₁)
-weak {Δ} {Γ} {A} {Γ'} (∧ₑ₂ x) x₁ = ∧ₑ₂ (weak x x₁)
-weak {Δ} {Γ} {A} {Γ'} (∨ᵢ₁ x) x₁ = ∨ᵢ₁ (weak x x₁)
-weak {Δ} {Γ} {A} {Γ'} (∨ᵢ₂ x) x₁ = ∨ᵢ₂ (weak x x₁)
-weak {Δ} {Γ} {A} {Γ'} (∨ₑ x x₂ x₃) x₁ = ∨ₑ (weak x x₁) (weak x₂ (inBoth x₁)) (weak x₃ (inBoth x₁))
-weak {Δ} {Γ} {A} {Γ'} (⇒ᵢ x) x₁ = ⇒ᵢ (weak x (inBoth x₁))
-weak {Δ} {Γ} {A} {Γ'} (¬ᵢ x) x₁ = ¬ᵢ (weak x (inBoth x₁))
-weak {Δ} {Γ} {A} {Γ'} (¬ₑ x x₂) x₁ = ¬ₑ (weak x x₁) (weak x₂ x₁)
-weak {Δ} {Γ} {A} {Γ'} (⊥ₑ x) x₁ = ⊥ₑ (weak x x₁)
-weak {Δ} {Γ} {A} {Γ'} (□ᵢ x) x₁ = □ᵢ x
-weak {Δ} {Γ} {A} {Γ'} (□ₑ x x₂) x₁ = □ₑ (weak x x₁) (weak x₂ x₁)
+weak (var x) x₁ = var (x₁ x)
+weak (mp x x₂) x₁ = mp (weak x x₁) (weak x₂ x₁)
+weak (∧ᵢ x x₂) x₁ = ∧ᵢ (weak x x₁) (weak x₂ x₁)
+weak (∧ₑ₁ x) x₁ = ∧ₑ₁ (weak x x₁)
+weak (∧ₑ₂ x) x₁ = ∧ₑ₂ (weak x x₁)
+weak (∨ᵢ₁ x) x₁ = ∨ᵢ₁ (weak x x₁)
+weak (∨ᵢ₂ x) x₁ = ∨ᵢ₂ (weak x x₁)
+weak (∨ₑ x x₂ x₃) x₁ = ∨ₑ (weak x x₁) (weak x₂ (inBoth x₁)) (weak x₃ (inBoth x₁))
+weak (⇒ᵢ x) x₁ = ⇒ᵢ (weak x (inBoth x₁))
+weak (¬ᵢ x) x₁ = ¬ᵢ (weak x (inBoth x₁))
+weak (¬ₑ x x₂) x₁ = ¬ₑ (weak x x₁) (weak x₂ x₁)
+weak (⊥ₑ x) x₁ = ⊥ₑ (weak x x₁)
+weak (□ᵢ x) x₁ = □ᵢ x
+weak (□ₑ x x₂) x₁ = □ₑ (weak x x₁) (weak x₂ x₁)
 
 weak-modal : Δ / Γ ⊢ A → Δ ⊆ Δ' → Δ' / Γ ⊢ A
 weak-modal (var x) x₁ = var x