diff --git a/mambo.agda b/mambo.agda
index 9bedd73..d54bcc4 100644
--- a/mambo.agda
+++ b/mambo.agda
@@ -285,3 +285,25 @@ ExampleSyn3 {A} {B} = ⇒ᵢ (□ₑ (∧ₑ₁ (var (zero ((□ A) ∧ (□ B))
 ExampleSyn4 : ∙ / ∙ ⊢ □ (A ⇒ B) ⇒ (◇ A ⇒ ◇ B)
 ExampleSyn4 {A} {B} = ⇒ᵢ (⇒ᵢ (¬ᵢ (□ₑ (var (zero (□ (∼ B)) (∙ , (□ (A ⇒ B)) , (◇ A)))) (□ₑ (var (succ (□ (A ⇒ B)) (∙ , (□ (A ⇒ B)) , (◇ A)) (succ (□ (A ⇒ B)) (∙ , (□ (A ⇒ B))) (zero (□ (A ⇒ B)) ∙)))) (¬ₑ (var (succ (∼ (□ (∼ A))) (∙ , (□ (A ⇒ B)) , (◇ A))
                                                                                                                                                                                                                       (zero (∼ (□ (∼ A))) (∙ , (□ (A ⇒ B)))))) (□ᵢ (¬ᵢ (¬ₑ (var (succ ( ∼ B) (∙ , (∼ B) , (A ⇒ B)) (succ (∼ B) (∙ , (∼ B)) (zero (∼ B) ∙)))) (mp (var (succ (A ⇒ B) (∙ , (∼ B) , (A ⇒ B)) (zero (A ⇒ B) (∙ , (∼ B))))) (var (zero A (∙ , (∼ B) , (A ⇒ B)))))))))))))
+
+ExampleSyn5 : ∙ / ∙ ⊢ □ ( A ⇒ B ) ⇒ ( □ A ⇒ □ B )
+ExampleSyn5 {A} {B} = ⇒ᵢ (⇒ᵢ (□ₑ (var (zero (□ A) (∙ , (□ (A ⇒ B))))) (□ₑ (var (succ (□ (A ⇒ B)) (∙ , (□ (A ⇒ B))) (zero (□ (A ⇒ B)) ∙))) (□ᵢ (mp (var (zero (A ⇒ B) (∙ , A))) (var (succ A (∙ , A) (zero A ∙))))))))
+
+ExampleSyn6 : ∙ / ∙ ⊢ (◇ A) ⇔ (∼ □ ∼ A)
+ExampleSyn6 {A} = ∧ᵢ (⇒ᵢ (var (zero (∼ (□ (∼ A))) ∙))) (⇒ᵢ (var (zero (◇ A) ∙)))
+
+ExampleSyn7 : ∙ / ∙ ⊢ □ A ⇒ (◇ (A ⇒ B) ⇒ ◇ B)
+ExampleSyn7 {A} {B} = ⇒ᵢ (⇒ᵢ (□ₑ (var (succ (□ A) (∙ , (□ A)) (zero (□ A) ∙))) (¬ᵢ (□ₑ (var (zero (□ (∼ B)) (∙ , (□ A) , (◇ (A ⇒ B))))) (¬ₑ (var (succ (∼ (□ (∼ (A ⇒ B)))) (∙ , (□ A) , (◇ (A ⇒ B)))
+                                                                                                                                                   (zero (∼ (□ (∼ (A ⇒ B)))) (∙ , (□ A))))) (□ᵢ (¬ᵢ (¬ₑ (var (succ (∼ B) (∙ , A , (∼ B)) (zero (∼ B) (∙ , A)))) (mp (var (zero (A ⇒ B) (∙ , A , (∼ B)))) (var (succ A (∙ , A , (∼ B)) (succ A (∙ , A) (zero A ∙)))))))))))))
+
+ExampleSyn8 : ∙ / ∙ ⊢ □ ∼ A ⇒ □ (A ⇒ B)
+ExampleSyn8 {A} {B} = ⇒ᵢ (□ₑ (var (zero (□ (∼ A)) ∙)) (□ᵢ (⇒ᵢ (⊥ₑ (¬ₑ (var (succ (∼ A) (∙ , (∼ A)) (zero (∼ A) ∙))) (var (zero A (∙ , (∼ A)))))))))
+
+ExampleSyn9 : ∙ / ∙ ⊢ (□ A) ∨ (□ B) ⇒ □ (A ∨ B)
+ExampleSyn9 {A} {B} = ⇒ᵢ (∨ₑ (var (zero ((□ A) ∨ (□ B)) ∙)) (□ₑ (var (zero (□ A) (∙ , ((□ A) ∨ (□ B))))) (□ᵢ (∨ᵢ₁ (var (zero A ∙))))) (□ₑ (var (zero (□ B) (∙ , ((□ A) ∨ (□ B))))) (□ᵢ (∨ᵢ₂ (var (zero B ∙))))))
+
+ExampleSyn10 : ∙ / ∙ ⊢ ◇ A ⇒ ◇ (A ∨ B)
+ExampleSyn10 {A} {B} = ⇒ᵢ (¬ᵢ (□ₑ (var (zero (□ (∼ (A ∨ B))) (∙ , (◇ A)))) (¬ₑ (var (succ ( ◇ A) (∙ , (◇ A)) (zero (∼ (□ (∼ A))) ∙))) (□ᵢ (¬ᵢ (¬ₑ (var (succ (∼ (A ∨ B)) (∙ , (∼ (A ∨ B))) (zero (∼ (A ∨ B)) ∙))) (∨ᵢ₁ (var (zero A (∙ , (∼ (A ∨ B))))))))))))
+
+ExampleSyn11 : ∙ / ∙ ⊢ ◇ A ⇒ □ B ⇒ □ ( A ⇒ B )
+ExampleSyn11 {A} {B} = ⇒ᵢ (⇒ᵢ (□ₑ (var (zero (□ B) (∙ , (◇ A)))) (□ᵢ (⇒ᵢ (var (succ B (∙ , B) (zero B ∙)))))))