diff --git a/FirstOrderLogic.agda b/FirstOrderLogic.agda
new file mode 100644
index 0000000..72f9519
--- /dev/null
+++ b/FirstOrderLogic.agda
@@ -0,0 +1,30 @@
+{-# OPTIONS --prop #-}
+
+open import Agda.Builtin.Nat
+
+module FirstOrderLogic (TV : Set) (F : Nat → Set) (R : Nat → Set) where
+
+  open import PropUtil
+  open import ListUtil
+
+  mutual
+    data FArgs : Nat → Set where
+      zero : FArgs 0
+      next : {n : Nat} → FArgs n → Term → FArgs (suc n)
+    data Term : Set where
+      Var : TV → Term
+      Fun : {n : Nat} → F n → FArgs n → Term
+      
+  data RArgs : Nat → Set where
+    zero : RArgs 0
+    next : {n : Nat} → RArgs n → Term → RArgs (suc n)
+    
+  data Form : Set where
+    Rel : {n : Nat} → R n → (RArgs n) → Form
+    _⇒_ : Form → Form → Form
+    _∧∧_ : Form → Form → Form
+    _∀∀_ : TV → Form → Form
+    
+  infixr 10 _∧∧_
+  infixr 8 _⇒_
+
diff --git a/ListUtil.agda b/ListUtil.agda
index d54c224..1a7bcd9 100644
--- a/ListUtil.agda
+++ b/ListUtil.agda
@@ -3,7 +3,7 @@
 module ListUtil where
 
   open import Data.List using (List; _∷_; []) public
-
+  
   private
     variable
       T : Set₀
@@ -138,3 +138,4 @@ module ListUtil where
 
   ⊆→∈* : L ⊆ L' → L ∈* L'
   ⊆→∈* h = ⊂⁺→∈* (⊂→⊂⁺ (⊆→⊂ h))
+