diff --git a/lib/Convert.ml b/lib/Core/Convert.ml
similarity index 100%
rename from lib/Convert.ml
rename to lib/Core/Convert.ml
diff --git a/lib/Eval.ml b/lib/Core/Eval.ml
similarity index 97%
rename from lib/Eval.ml
rename to lib/Core/Eval.ml
index 82df1ab..4977293 100644
--- a/lib/Eval.ml
+++ b/lib/Core/Eval.ml
@@ -39,6 +39,7 @@ let rec eval (env : V.env) (tr : T.term) =
   | Pair (x, y)               -> V.Pair (eval env x, eval env y)
   | Fst  tr                   -> fst (eval env tr)
   | Snd  tr                   -> snd (eval env tr)
+  | Let  (tr, _, B sc)        -> eval (eval env tr :: env) sc
 
 (* B b, B B ts *)
 and indN (env : V.env) (b : T.term) (tz : V.value) (ts : T.term) (n : V.value) =
diff --git a/lib/Term.ml b/lib/Core/Term.ml
similarity index 90%
rename from lib/Term.ml
rename to lib/Core/Term.ml
index b509b6c..1fa1886 100644
--- a/lib/Term.ml
+++ b/lib/Core/Term.ml
@@ -31,3 +31,5 @@ type term
   | Pair of term * term
   | Fst  of term
   | Snd  of term
+
+  | Let  of term * term * term binder (* tr : ty in sc *)
diff --git a/lib/Value.ml b/lib/Core/Value.ml
similarity index 100%
rename from lib/Value.ml
rename to lib/Core/Value.ml
diff --git a/lib/Core/dune b/lib/Core/dune
new file mode 100644
index 0000000..a27e659
--- /dev/null
+++ b/lib/Core/dune
@@ -0,0 +1,2 @@
+(library
+ (name Core))
diff --git a/lib/Parse/dune b/lib/Parse/dune
new file mode 100644
index 0000000..405a68d
--- /dev/null
+++ b/lib/Parse/dune
@@ -0,0 +1,10 @@
+(library
+ (name Parse)
+ (flags (:standard -w -27 -w -39 -w -33)))
+(rule
+  (alias bnfc)
+  (deps "implicitt.cf")
+  (targets AbsImplicitt.ml BNFC_Util.ml LexImplicitt.mll ParImplicitt.mly PrintImplicitt.ml ShowImplicitt.ml SkelImplicitt.ml TestImplicitt.ml)
+  (action (system "bnfc --ocaml implicitt.cf")))
+(ocamllex LexImplicitt)
+(ocamlyacc ParImplicitt)
diff --git a/lib/Parse/implicitt.cf b/lib/Parse/implicitt.cf
new file mode 100644
index 0000000..e22f696
--- /dev/null
+++ b/lib/Parse/implicitt.cf
@@ -0,0 +1,60 @@
+entrypoints [Def], Term;
+
+token Id ((letter|digit|["[]_"])+) ;
+
+comment "--" ;
+comment "{-" "-}" ;
+
+Defn. Def ::= "def" Id ":" Term ":=" Term;
+separator nonempty Def "" ;
+
+-- names bound by lambdas
+NImp.   Name ::= "{" Id "}";
+NExp.   Name ::= Id;
+separator nonempty Name "" ;
+
+-- Term 2
+TVar.   Term2 ::= Id;
+
+TType.  Term2 ::= "Type";
+
+TT0.    Term2 ::= "𝟘";
+
+TT1.    Term2 ::= "𝟙";
+TT1tr.  Term2 ::= "★";
+
+TBool.  Term2 ::= "𝟚";
+TTrue.  Term2 ::= "true";
+TFalse. Term2 ::= "false";
+
+TNat.   Term2 ::= "ℕ";
+TZero.  Term2 ::= "0";
+
+TLam.   Term2 ::= "λ" [Name] "." Term;
+
+-- Term1
+TInd0.  Term1 ::= "𝟘-elim" Term2 Term2;
+
+TIndB.  Term1 ::= "𝟚-elim" Term2 Term2 Term2 Term2;
+
+TSuc.   Term1 ::= "suc" Term2;
+TIndN.  Term1 ::= "ℕ-elim" Term2 Term2 Term2 Term2;
+
+TFst.   Term1 ::= "pr₁" Term2;
+TSnd.   Term1 ::= "pr₂" Term2;
+
+TApp.   Term1 ::= Term1 Term2;
+
+-- Term0
+TLet.   Term ::= "let" Id ":" Term ":=" Term "in" Term ;
+
+TPiAr.  Term ::= Term "→" Term;
+TPiEx.  Term ::= "(" Id ":" Term ")" "→" Term;
+TPiIm.  Term ::= "{" Id ":" Term "}" "→" Term;
+
+TSgCr.  Term ::= Term "×" Term;
+TSg.    Term ::= "(" Id ":" Term ")" "×" Term;
+TPair.  Term ::= "⟨" Term "," Term "⟩";
+
+
+coercions Term 2;
diff --git a/lib/dune b/lib/dune
deleted file mode 100644
index c76f468..0000000
--- a/lib/dune
+++ /dev/null
@@ -1,2 +0,0 @@
-(library
- (name implicitt))