diff --git a/mambo.agda b/mambo.agda
index 5fbdabe..e0632ca 100644
--- a/mambo.agda
+++ b/mambo.agda
@@ -145,3 +145,12 @@ ExampleSyn2 {A} {B} = ⇒ᵢ (∧ᵢ (□ₑ (var (zero (□ (A ∧ B)) [])) (
 
 ExampleSyn3 : [] / [] ⊢ (□ A ∧ □ B) ⇒ □(A ∧ B)
 ExampleSyn3 {A} {B} = ⇒ᵢ (□ₑ (∧ₑ₁ (var (zero ((□ A) ∧ (□ B)) []))) (□ₑ (∧ₑ₂ (var (zero ((□ A) ∧ (□ B)) []))) (□ᵢ (∧ᵢ (var (succ A ([] , A) (zero A []))) (var (zero B ([] , A)))))))
+
+ExampleSyn4 : [] / [] ⊢ □ (A ⇒ B) ⇒ (◇ A ⇒ ◇ B)
+ExampleSyn4 {A} {B} = {!!}
+
+Soundness : {W : Type} → (p : Formula) → [] / [] ⊢ p → (∀ (m : M W) (x : W) → m , x ⊩ p)
+Soundness p x m w = {!!}
+
+Completeness : {W : Type} → (p : Formula) → (∀ (m : M W) (x : W) → m , x ⊩ p) → [] / [] ⊢ p
+Completeness p x = {!!}