diff --git a/lib/formula.ml b/lib/formula.ml
index 2daad88..e4b7d57 100644
--- a/lib/formula.ml
+++ b/lib/formula.ml
@@ -1,11 +1,11 @@
 type t =
-    | Relation of string * Term.t list
-    | Equal of Term.t * Term.t
-    | Bottom
-    | Neg of t
-    | Conj of t * t
-    | Disj of t * t
-    | Impl of t * t
-    | Iff of t * t
-    | Forall of t
-    | Exists of t
+  | Relation of string * Term.t list
+  | Equal of Term.t * Term.t
+  | Bottom
+  | Neg of t
+  | Conj of t * t
+  | Disj of t * t
+  | Impl of t * t
+  | Iff of t * t
+  | Forall of t
+  | Exists of t
diff --git a/lib/formula.mli b/lib/formula.mli
index 2daad88..e4b7d57 100644
--- a/lib/formula.mli
+++ b/lib/formula.mli
@@ -1,11 +1,11 @@
 type t =
-    | Relation of string * Term.t list
-    | Equal of Term.t * Term.t
-    | Bottom
-    | Neg of t
-    | Conj of t * t
-    | Disj of t * t
-    | Impl of t * t
-    | Iff of t * t
-    | Forall of t
-    | Exists of t
+  | Relation of string * Term.t list
+  | Equal of Term.t * Term.t
+  | Bottom
+  | Neg of t
+  | Conj of t * t
+  | Disj of t * t
+  | Impl of t * t
+  | Iff of t * t
+  | Forall of t
+  | Exists of t
diff --git a/lib/proof.ml b/lib/proof.ml
index e69de29..52b5264 100644
--- a/lib/proof.ml
+++ b/lib/proof.ml
@@ -0,0 +1,64 @@
+type label =
+  | Axiom
+  | AndI
+  | AndE
+  | OrI
+  | OrE
+  | ArrI
+  | ArrE
+  | NegI
+  | NegE
+  | RAA
+  | IffI
+  | IffE
+  | EqI
+  | EqE
+  | ForallI
+  | ForallE
+  | ExistsI
+  | ExistsE
+
+type pref = Linenum of int | Named of string
+type t = { children : pref list; label : label; formula : Formula.t }
+
+let rec valid res a { children; label; formula } =
+  let children = List.map res children in
+  match (children, label, formula) with
+  | [], Axiom, phi -> List.mem phi a
+  | [ left; right ], AndI, Conj (phi, psi) ->
+      left.formula = phi && right.formula = psi && valid res a left
+      && valid res a right
+  | [ ({ formula = Conj (phi, psi); _ } as kid) ], AndE, chi ->
+      (chi = phi || chi = psi) && valid res a kid
+  | [ kid ], OrI, Disj (phi, psi) ->
+      (kid.formula = phi || kid.formula = psi) && valid res a kid
+  | [ ({ formula = Disj (phi, psi); _ } as left); middle; right ], OrE, chi ->
+      middle.formula = chi && right.formula = chi && valid res a left
+      && valid res (phi :: a) middle
+      && valid res (psi :: a) right
+  | [ kid ], ArrI, Impl (phi, psi) ->
+      kid.formula = psi && valid res (phi :: a) kid
+  | [ left; right ], ArrE, psi ->
+      left.formula = Impl (right.formula, psi)
+      && valid res a left && valid res a right
+  | [ kid ], NegI, Neg phi -> kid.formula = Bottom && valid res (phi :: a) kid
+  | [ left; right ], NegE, Bottom ->
+      left.formula = Neg right.formula && valid res a left && valid res a right
+  | [ kid ], RAA, phi -> kid.formula = Bottom && valid res (Neg phi :: a) kid
+  | [ left; right ], IffI, Iff (phi, psi) ->
+      left.formula = Impl (phi, psi)
+      && right.formula = Impl (psi, phi)
+      && valid res a left && valid res a right
+  | [ left; right ], IffE, phi ->
+      (left.formula = Iff (right.formula, phi)
+      || left.formula = Iff (phi, right.formula))
+      && valid res a left && valid res a right
+  | [], EqI, Equal (x, y) -> x = y
+
+(* TODO:
+   - EqE
+   - ForallI
+   - ForallE
+   - ExistsI
+   - ExistsE
+*)
diff --git a/lib/proof.mli b/lib/proof.mli
index e69de29..277369a 100644
--- a/lib/proof.mli
+++ b/lib/proof.mli
@@ -0,0 +1,24 @@
+type label =
+  | Axiom
+  | AndI
+  | AndE
+  | OrI
+  | OrE
+  | ArrI
+  | ArrE
+  | NegI
+  | NegE
+  | RAA
+  | IffI
+  | IffE
+  | EqI
+  | EqE
+  | ForallI
+  | ForallE
+  | ExistsI
+  | ExistsE
+
+type pref = Linenum of int | Named of string
+type t = { children : pref list; label : label; formula : Formula.t }
+
+val valid : (pref -> t) -> Formula.t list -> t -> bool
diff --git a/lib/term.ml b/lib/term.ml
index 252d267..5d9027d 100644
--- a/lib/term.ml
+++ b/lib/term.ml
@@ -1,5 +1,5 @@
 type t =
-    | Var of int
-    | Const of string
-    | Free of string
-    | Function of string * t list
+  | Var of int
+  | Const of string
+  | Free of string
+  | Function of string * t list
diff --git a/lib/term.mli b/lib/term.mli
index 252d267..5d9027d 100644
--- a/lib/term.mli
+++ b/lib/term.mli
@@ -1,5 +1,5 @@
 type t =
-    | Var of int
-    | Const of string
-    | Free of string
-    | Function of string * t list
+  | Var of int
+  | Const of string
+  | Free of string
+  | Function of string * t list