From 309ba6ab7064ae20f2e8e87ea752dc26aa231ccc Mon Sep 17 00:00:00 2001
From: Thorsten Altenkirch <txa@cs.nott.ac.uk>
Date: Tue, 20 Jun 2023 15:36:18 +0200
Subject: [PATCH] added examples

---
 fol.agda | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/fol.agda b/fol.agda
index e2ecc68..678232a 100644
--- a/fol.agda
+++ b/fol.agda
@@ -77,5 +77,10 @@ example {A = A} = lam (lam (App (app (suc zero)
            (wk-subst {A = A}) (App zero zero))) zero))
 
 
+-- (∀ x ∀ y . A(x,y)) ⇒ ∀ y ∀ x . A(y,x)
+-- (A ⇒ ∀ x . B(x)) ⇒ ∀ x . A ⇒ B(x)   
+-- ∀ x y . A(x,y) ⇒ ∀ x . A(x,x)
+-- ∀ x . A (x) ⇒ ∀ x y . A(x)
+-- (((∀ x . A (x)) ⇒ B)⇒ B) ⇒ ∀ x . ((A (x) ⇒ B) ⇒ B)
 
 -}