diff --git a/lib/Raw/PostProcess.ml b/lib/Raw/PostProcess.ml
new file mode 100644
index 0000000..c481486
--- /dev/null
+++ b/lib/Raw/PostProcess.ml
@@ -0,0 +1,4 @@
+module A = AbsImplicitt
+module R = RawSyntax
+
+open R
diff --git a/lib/Raw/RawSyntax.ml b/lib/Raw/RawSyntax.ml
index 3367528..92abd2c 100644
--- a/lib/Raw/RawSyntax.ml
+++ b/lib/Raw/RawSyntax.ml
@@ -8,8 +8,6 @@ type icit
 type ast
   = Var of var
 
-  | Test of A.exp
-
   | Type
 
   | T0
diff --git a/lib/Raw/dune b/lib/Raw/dune
index 93ed14e..60b03fa 100644
--- a/lib/Raw/dune
+++ b/lib/Raw/dune
@@ -15,4 +15,9 @@
 
 (library
  (name Raw)
- (modules AbsImplicitt BNFC_Util LexImplicitt ParImplicitt RawSyntax))
+ (modules AbsImplicitt
+          BNFC_Util
+          LexImplicitt
+          ParImplicitt
+          RawSyntax
+          PostProcess))
diff --git a/lib/Raw/implicitt.cf b/lib/Raw/implicitt.cf
index 58f8f14..123fc5e 100644
--- a/lib/Raw/implicitt.cf
+++ b/lib/Raw/implicitt.cf
@@ -14,7 +14,8 @@ ExpPiI.    Exp  ::= "Π" "{" Id ":" Exp "}" Exp;
 ExpSig.    Exp  ::= "Σ" "(" Id ":" Exp ")" Exp;
 ExpLet.    Exp  ::= "let" Id ":" Exp ":=" Exp "in" Exp;
 ExpLam.    Exp  ::= "λ" [BD] "." Exp;
-ExpApp.    Exp1 ::= Exp1 Exp2;
+ExpAppI.   Exp1 ::= Exp1 "{" Exp "}";
+ExpAppE.   Exp1 ::= Exp1 Exp2;
 ExpVar.    Exp2 ::= Id;
 ExpT0.     Exp2 ::= "⊥";
 ExpT1.     Exp2 ::= "⊤";
@@ -29,6 +30,8 @@ ExpTPair.  Exp2 ::= "⟨" Exp "," Exp "⟩";
 ExpTFst.   Exp2 ::= "pr₁";
 ExpTSnd.   Exp2 ::= "pr₂";
 
+coercions Exp 2 ;
+
 VarDef. Def ::= "def" Id ":" Exp ":=" Exp;
 
-separator Def ";" ;
\ No newline at end of file
+separator Def "" ;
\ No newline at end of file