diff --git a/doc/lfsc1_5.g4 b/doc/lfsc1_5.g4
index 3452c4a..fef8e3e 100644
--- a/doc/lfsc1_5.g4
+++ b/doc/lfsc1_5.g4
@@ -17,8 +17,10 @@ command
   | '(' 'run' code ')'
   | '(' 'program' iden '(' typed_par+ ')' type code ')'
 // Extension /////////////////////////////////
-  | '(' 'declare-type' iden '(' type* ')' ')'
-  | '(' 'declare-rule' iden ( ntype | vtype )+ type ')' ')'
+  | '(' 'declare-type' iden decl_list ')'
+  | '(' 'declare-rule' iden decl_list type ')'
+  | '(' 'define-const' iden decl_list term ')'
+  | '(' 'check-assuming' decl_list type term ')'
 //////////////////////////////////////////////
   ;
 // (declare-type c (τ₁ ⋯ τᵢ)) with i > 0
@@ -33,6 +35,8 @@ command
 // is equivalent to
 // (declare r (-> r ν₁ ⋯ νᵢ τ))
 
+decl_list : '(' (ntype | vtype)* ')';
+
 iden : ID ;
 
 kind 
@@ -78,7 +82,7 @@ ntype
 // (^ c t)
 
 // Extension /////////////////////
-vtype : '(' 'var' iden ntype ')' ;
+vtype : '(' ':' iden ntype ')' ;
 //////////////////////////////////
 
 type 
@@ -89,7 +93,7 @@ type
   | '(' '!' iden ntype type ')' 
 // Extension ///////////////////////////////
   | '(' 'Forall' iden ntype type ')' 
-  | '(' '->' ( ntype | vtype )+ type ')'  
+  | '(' '->' decl_list type ')'  
 ////////////////////////////////////////////
   ;
 // (Forall ξ τ₁ τ₂)
@@ -117,14 +121,13 @@ term
   | rat_const
   | '(' term term+ ')'
   | '(' '\\' iden term ')'
-  | '(' '@' iden term ')'
+  | '(' '@' iden term term ')'
   | '(' ':' type term ')'
+  // Deprecated
   | '(' '%' iden type term ')'
 // Extensions ///////////////////
   | '(' 'lam' iden term ')'
   | '(' 'let' iden term term ')'
-  | '(' 'proved-by' type term ')'
-  | '(' 'assuming' vtype+ term ')'
   ;
 //////////////////////////////////
 // (lam ξ t)
@@ -167,4 +170,4 @@ code
 INT : [0-9]+ ;
 RAT : ('0' | [1-9][0-9]*) '/' [1-9][0-9]* ;
 ID : [a-zA-Z~!@$%^&*_\-+=<>.?/][a-zA-Z0-9~!@$%^&*_\-+=<>.?/]* ;
-KW : ':'[a-zA-Z0-9~!@$%^&*_\-+=<>.?/]* ; 
\ No newline at end of file
+KW : ':'[a-zA-Z0-9~!@$%^&*_\-+=<>.?/]* ;