diff --git a/README.md b/README.md
index e97500e..7961533 100644
--- a/README.md
+++ b/README.md
@@ -10,6 +10,11 @@ A "proof assistant" with holes and implicit arguments. Developed to learn about
 
 # TODO
 
+* Figure out representation of metas
+  * Types needed for stuck values and typed conversion
+  * Meta has value or other meta for type?
+  * Where to put this file?
+
 * Raw syntax
   * Parser (BNFC)
 
diff --git a/bin/dune b/bin/dune
index b6a52d7..a2f789e 100644
--- a/bin/dune
+++ b/bin/dune
@@ -1,4 +1,4 @@
 (executable
  (public_name implicitt)
  (name main)
- (libraries Core Raw Parse))
+ (libraries Core Raw))
diff --git a/lib/Core/Common.ml b/lib/Core/Common.ml
new file mode 100644
index 0000000..3544cd5
--- /dev/null
+++ b/lib/Core/Common.ml
@@ -0,0 +1,10 @@
+(* number ; is-hole? *)
+type meta = Mv of int * bool
+
+
+let cMV : int ref = ref 0
+
+let getCMV (_ : unit) =
+  let c = ! cMV in
+  cMV.contents <- c + 1;
+  c
diff --git a/lib/Core/Eval.ml b/lib/Core/Eval.ml
index 4977293..36d1a55 100644
--- a/lib/Core/Eval.ml
+++ b/lib/Core/Eval.ml
@@ -9,6 +9,7 @@ let rec index (env : V.env) (i : int) =
 let rec eval (env : V.env) (tr : T.term) =
   match tr with
   | Var  (Ix i)               -> index env i
+  | Mv   m                    -> V.Stuck (V.Meta m, ?)
   | Type                      -> V.Type
   | T0                        -> V.T0
   | Ind0 (B b, t)             -> begin
diff --git a/lib/Core/Term.ml b/lib/Core/Term.ml
index 8fc5af6..a7cd614 100644
--- a/lib/Core/Term.ml
+++ b/lib/Core/Term.ml
@@ -1,9 +1,12 @@
+module C = Common
+
 type var = Ix of int
 
 type 'a binder = B of 'a
 
 type term 
   = Var  of var
+  | Meta of C.meta
 
   | Type
 
diff --git a/lib/Core/Value.ml b/lib/Core/Value.ml
index 07e3958..1fa188d 100644
--- a/lib/Core/Value.ml
+++ b/lib/Core/Value.ml
@@ -1,6 +1,7 @@
 module T = Term
+module C = Common
 
-type lvl = Lvl of int
+type lvl  = Lvl of int
 
 type closure  = C  of env * T.term
 and  closure2 = C2 of env * T.term (* 2 variables missing *)
@@ -26,6 +27,7 @@ and value
 
 and stuck
   = Var  of lvl
+  | Meta of C.meta
   | Ind0 of closure * stuck
   | IndN of closure * value * closure2 * stuck
   | IndB of closure * value * value * stuck
diff --git a/lib/Raw/PostProcess.ml b/lib/Raw/PostProcess.ml
index 376c171..3592458 100644
--- a/lib/Raw/PostProcess.ml
+++ b/lib/Raw/PostProcess.ml
@@ -1,5 +1,6 @@
 module P = AbsImplicitt
 module R = RawSyntax
+module C = Common
 
 open R
 
@@ -33,7 +34,17 @@ let rec proc (e : P.id list) (ex : P.exp) =
   | ExpPair (e1, e2) -> Pair (proc e e1, proc e e2)
   | ExpFst e1 -> Fst (proc e e1)
   | ExpSnd e1 -> Snd (proc e e1)
-  | ExpHole -> failwith "hole not implemented"
+  | ExpHole -> C.Mv (getCMV (), true)
+  | ExpInd0 (Id i1, e1, e2) -> Ind0 (B (proc (i1 :: e)) e1) e2
+  | ExpIndN (Id i1, e1, e2, Id i2, Id i3, e3, e4) ->
+     IndN (B (proc (i1 :: e) e1)) (proc e e2)
+       (B (B (proc (i3 :: i2 :: e) e3)))
+       (proc e e4)
+  | ExpIndB (Id i1, e1, e2, e3, e4) ->
+     IndB (B (proc (i1 :: e) e1))
+       (proc e e2)
+       (proc e e3)
+       (proc e e4)
 
 and unwrapLambda (e : P.id list) (bs : P.bD list) (sc : P.exp) =
   match bs with
diff --git a/lib/Raw/dune b/lib/Raw/dune
index 60b03fa..1f9a565 100644
--- a/lib/Raw/dune
+++ b/lib/Raw/dune
@@ -15,6 +15,7 @@
 
 (library
  (name Raw)
+ (libraries Core)
  (modules AbsImplicitt
           BNFC_Util
           LexImplicitt
diff --git a/lib/Raw/implicitt.cf b/lib/Raw/implicitt.cf
index 9e2dff1..9e73a8c 100644
--- a/lib/Raw/implicitt.cf
+++ b/lib/Raw/implicitt.cf
@@ -19,6 +19,15 @@ ExpAppE.   Exp1 ::= Exp1 Exp2;
 ExpFst.    Exp1 ::= "pr₁" Exp2;
 ExpSnd.    Exp1 ::= "pr₂" Exp2;
 ExpSuc.    Exp1 ::= "S" Exp2;
+
+ExpInd0.   Exp1 ::= "⊥-elim" "⟦" Id "⇒" Exp "⟧" Exp2;
+ExpIndN.   Exp1 ::= "ℕ-elim" "⟦" Id        "⇒" Exp "⟧"
+                             "⟦" "0"       "⇒" Exp
+			     "," "S" Id Id "⇒" Exp "⟧" Exp2;
+ExpIndB.   Exp1 ::= "𝔹-elim" "⟦" Id  "⇒" Exp "⟧"
+                             "⟦" "T" "⇒" Exp
+			     "," "F" "⇒" Exp "⟧" Exp2;
+
 ExpVar.    Exp2 ::= Id;
 ExpT0.     Exp2 ::= "⊥";
 ExpT1.     Exp2 ::= "⊤";
@@ -31,6 +40,7 @@ ExpFalse.  Exp2 ::= "F";
 ExpPair.   Exp2 ::= "⟨" Exp "," Exp "⟩";
 ExpHole.   Exp2 ::= "?";
 
+
 coercions Exp 2 ;
 
 VarDef. Def ::= "def" Id ":" Exp "≔" Exp;