diff --git a/src/eval_nat_exp/mod.rs b/src/eval_nat_exp/mod.rs
new file mode 100644
index 0000000..9eefe6b
--- /dev/null
+++ b/src/eval_nat_exp/mod.rs
@@ -0,0 +1 @@
+pub mod proofs;
diff --git a/src/eval_nat_exp/proofs.rs b/src/eval_nat_exp/proofs.rs
new file mode 100644
index 0000000..3617b72
--- /dev/null
+++ b/src/eval_nat_exp/proofs.rs
@@ -0,0 +1,12 @@
+use super::super::nat::proofs::*;
+use super::super::nat::Nat;
+
+pub enum ProofEvalNatExp {
+    EConst,
+    EPlus,
+    ETimes,
+    ProofPlusIs::PZero,
+    ProofPlusIs::PSucc(Box<ProofPlusIs>),
+    ProofTimeIs::TZero,
+    ProofTimeIs::TSucc(Box<ProofTimeIs>, Box<ProofPlusIs>, Nat),
+}