diff --git a/src/lib/ModelConverter.ml b/src/lib/ModelConverter.ml
index e8474f06..46c46cd3 100644
--- a/src/lib/ModelConverter.ml
+++ b/src/lib/ModelConverter.ml
@@ -2769,9 +2769,10 @@ let convert_property_option (useful_parsing_model_information : useful_parsing_m
 (*------------------------------------------------------------*)
 (** Convert the parsed model and the parsed property into an abstract model and an abstract property *)
 (*------------------------------------------------------------*)
-let abstract_structures_of_parsing_structures options (parsed_model : ParsingStructure.unexpanded_parsed_model) (parsed_property_option : ParsingStructure.parsed_property option) : AbstractModel.abstract_model * (AbstractProperty.abstract_property option) =
+let abstract_structures_of_parsing_structures options (parsed_model : ParsingStructure.unexpanded_parsed_model) (parsed_property_option : ParsingStructure.unexpanded_parsed_property option) : AbstractModel.abstract_model * (AbstractProperty.abstract_property option) =
 
   (* Instantiate the template calls and expand syntatic variables *)
+  let parsed_property_option = Option.map (expand_property parsed_model.unexpanded_variable_declarations) parsed_property_option in
   let parsed_model = expand_model parsed_model in
 
   print_message Verbose_high ("\n*** Link variables to declarations.");
diff --git a/src/lib/ModelConverter.mli b/src/lib/ModelConverter.mli
index 9b70a81a..6c040d93 100644
--- a/src/lib/ModelConverter.mli
+++ b/src/lib/ModelConverter.mli
@@ -34,4 +34,4 @@ exception InvalidProperty
 (* Conversion functions *)
 (****************************************************************)
 (** Convert the parsed model and the parsed property into an abstract model and an abstract property *)
-val abstract_structures_of_parsing_structures : Options.imitator_options -> ParsingStructure.unexpanded_parsed_model -> (ParsingStructure.parsed_property option) -> AbstractModel.abstract_model * (AbstractProperty.abstract_property option)
+val abstract_structures_of_parsing_structures : Options.imitator_options -> ParsingStructure.unexpanded_parsed_model -> (ParsingStructure.unexpanded_parsed_property option) -> AbstractModel.abstract_model * (AbstractProperty.abstract_property option)
diff --git a/src/lib/ParsingStructure.mli b/src/lib/ParsingStructure.mli
index 3a162c71..d247fe42 100644
--- a/src/lib/ParsingStructure.mli
+++ b/src/lib/ParsingStructure.mli
@@ -406,6 +406,10 @@ type parsed_loc_predicate =
 	| Parsed_loc_predicate_EQ of automaton_name * location_name
 	| Parsed_loc_predicate_NEQ of automaton_name * location_name
 
+type unexpanded_parsed_loc_predicate =
+	| Unexpanded_Parsed_loc_predicate_EQ of name_or_access * location_name
+	| Unexpanded_Parsed_loc_predicate_NEQ of name_or_access * location_name
+
 
 type parsed_simple_predicate =
 	| Parsed_discrete_boolean_expression of parsed_discrete_boolean_expression
@@ -414,6 +418,13 @@ type parsed_simple_predicate =
 	| Parsed_state_predicate_false
 	| Parsed_state_predicate_accepting
 
+type unexpanded_parsed_simple_predicate =
+	| Unexpanded_Parsed_discrete_boolean_expression of parsed_discrete_boolean_expression
+	| Unexpanded_Parsed_loc_predicate of unexpanded_parsed_loc_predicate
+	| Unexpanded_Parsed_state_predicate_true
+	| Unexpanded_Parsed_state_predicate_false
+	| Unexpanded_Parsed_state_predicate_accepting
+
 type parsed_state_predicate_factor =
 	| Parsed_state_predicate_factor_NOT of parsed_state_predicate_factor
 	| Parsed_simple_predicate of parsed_simple_predicate
@@ -427,6 +438,22 @@ and parsed_state_predicate =
 	| Parsed_state_predicate_OR of parsed_state_predicate * parsed_state_predicate
 	| Parsed_state_predicate_term of parsed_state_predicate_term
 
+type unexpanded_parsed_state_predicate_factor =
+	| Unexpanded_Parsed_state_predicate_factor_NOT of unexpanded_parsed_state_predicate_factor
+	| Unexpanded_Parsed_simple_predicate of unexpanded_parsed_simple_predicate
+	| Unexpanded_Parsed_state_predicate of unexpanded_parsed_state_predicate
+	(* The forall is in this level so we can use it on both sides of `AND` and `OR` *)
+	| Unexpanded_Parsed_forall_simple_predicate of forall_index_data * unexpanded_parsed_simple_predicate
+	| Unexpanded_Parsed_forall_state_predicate of forall_index_data * unexpanded_parsed_state_predicate
+
+and unexpanded_parsed_state_predicate_term =
+	| Unexpanded_Parsed_state_predicate_term_AND of unexpanded_parsed_state_predicate_term * unexpanded_parsed_state_predicate_term
+	| Unexpanded_Parsed_state_predicate_factor of unexpanded_parsed_state_predicate_factor
+
+and unexpanded_parsed_state_predicate =
+	| Unexpanded_Parsed_state_predicate_OR of unexpanded_parsed_state_predicate * unexpanded_parsed_state_predicate
+	| Unexpanded_Parsed_state_predicate_term of unexpanded_parsed_state_predicate_term
+
 	
 (****************************************************************)
 (* Parsed property *)
@@ -659,6 +686,48 @@ type parsed_property_type =
 	| Parsed_Win of parsed_state_predicate
 
 
+type unexpanded_parsed_property_type =
+	| Unexpanded_Parsed_Valid
+	| Unexpanded_Parsed_EF of unexpanded_parsed_state_predicate
+	| Unexpanded_Parsed_AGnot of unexpanded_parsed_state_predicate
+	| Unexpanded_Parsed_AG of unexpanded_parsed_state_predicate
+	| Unexpanded_Parsed_EG of unexpanded_parsed_state_predicate
+	| Unexpanded_Parsed_ER of unexpanded_parsed_state_predicate * unexpanded_parsed_state_predicate
+	| Unexpanded_Parsed_EU of unexpanded_parsed_state_predicate * unexpanded_parsed_state_predicate
+	| Unexpanded_Parsed_EW of unexpanded_parsed_state_predicate * unexpanded_parsed_state_predicate
+	| Unexpanded_Parsed_AF of unexpanded_parsed_state_predicate
+	| Unexpanded_Parsed_AR of unexpanded_parsed_state_predicate * unexpanded_parsed_state_predicate
+	| Unexpanded_Parsed_AU of unexpanded_parsed_state_predicate * unexpanded_parsed_state_predicate
+	| Unexpanded_Parsed_AW of unexpanded_parsed_state_predicate * unexpanded_parsed_state_predicate
+	| Unexpanded_Parsed_EF_timed of parsed_interval * unexpanded_parsed_state_predicate
+	| Unexpanded_Parsed_ER_timed of parsed_interval * unexpanded_parsed_state_predicate * unexpanded_parsed_state_predicate
+	| Unexpanded_Parsed_EU_timed of parsed_interval * unexpanded_parsed_state_predicate * unexpanded_parsed_state_predicate
+	| Unexpanded_Parsed_EW_timed of parsed_interval * unexpanded_parsed_state_predicate * unexpanded_parsed_state_predicate
+	| Unexpanded_Parsed_AF_timed of parsed_interval * unexpanded_parsed_state_predicate
+	| Unexpanded_Parsed_AR_timed of parsed_interval * unexpanded_parsed_state_predicate * unexpanded_parsed_state_predicate
+	| Unexpanded_Parsed_AU_timed of parsed_interval * unexpanded_parsed_state_predicate * unexpanded_parsed_state_predicate
+	| Unexpanded_Parsed_AW_timed of parsed_interval * unexpanded_parsed_state_predicate * unexpanded_parsed_state_predicate
+	| Unexpanded_Parsed_EFpmin of unexpanded_parsed_state_predicate * variable_name
+	| Unexpanded_Parsed_EFpmax of unexpanded_parsed_state_predicate * variable_name
+	| Unexpanded_Parsed_EFtmin of unexpanded_parsed_state_predicate
+	| Unexpanded_Parsed_Cycle_Through of unexpanded_parsed_state_predicate
+	| Unexpanded_Parsed_Cycle_Through_generalized of unexpanded_parsed_state_predicate list
+	| Unexpanded_Parsed_NZ_Cycle
+	| Unexpanded_Parsed_Deadlock_Freeness
+	| Unexpanded_Parsed_IM of parsed_pval
+	| Unexpanded_Parsed_ConvexIM of parsed_pval
+	| Unexpanded_Parsed_PRP of unexpanded_parsed_state_predicate * parsed_pval
+	| Unexpanded_Parsed_IMK of parsed_pval
+	| Unexpanded_Parsed_IMunion of parsed_pval
+	| Unexpanded_Parsed_Cover_cartography of parsed_pdomain * NumConst.t
+	| Unexpanded_Parsed_Learning_cartography of unexpanded_parsed_state_predicate * parsed_pdomain * NumConst.t
+	| Unexpanded_Parsed_Shuffle_cartography of parsed_pdomain * NumConst.t
+	| Unexpanded_Parsed_Border_cartography of parsed_pdomain * NumConst.t
+	| Unexpanded_Parsed_Random_cartography of parsed_pdomain * int * NumConst.t
+	| Unexpanded_Parsed_RandomSeq_cartography of parsed_pdomain * int * NumConst.t
+	| Unexpanded_Parsed_PRPC of unexpanded_parsed_state_predicate * parsed_pdomain * NumConst.t
+	| Unexpanded_Parsed_pattern of parsed_pattern
+	| Unexpanded_Parsed_Win of unexpanded_parsed_state_predicate
 
 type parsed_property = {
 	(* Emptiness or synthesis *)
@@ -669,6 +738,12 @@ type parsed_property = {
 	projection		: parsed_projection;
 }
 
+type unexpanded_parsed_property = {
+	unexpanded_synthesis_type	: parsed_synthesis_type;
+	unexpanded_property		: unexpanded_parsed_property_type;
+	unexpanded_projection		: parsed_projection;
+}
+
 type declarations_info = {
     clock_names : variable_name list;
     parameter_names : variable_name list;
diff --git a/src/lib/ParsingUtility.ml b/src/lib/ParsingUtility.ml
index 0e6bb694..ad17dedf 100644
--- a/src/lib/ParsingUtility.ml
+++ b/src/lib/ParsingUtility.ml
@@ -252,7 +252,7 @@ let compile_model_and_property (options : Options.imitator_options) =
 		print_message Verbose_low ("Parsing property file `" ^ property_file_name ^ "`…");
 		
 		(* Parsing the property *)
-		let parsed_property : ParsingStructure.parsed_property = parser_lexer_from_file Property options PropertyParser.main PropertyLexer.token property_file_name in
+		let parsed_property : ParsingStructure.unexpanded_parsed_property = parser_lexer_from_file Property options PropertyParser.main PropertyLexer.token property_file_name in
 
 		(* Statistics *)
 		parsing_counter#stop;
diff --git a/src/lib/PropertyLexer.mll b/src/lib/PropertyLexer.mll
index 1cdaa384..54eefc66 100644
--- a/src/lib/PropertyLexer.mll
+++ b/src/lib/PropertyLexer.mll
@@ -99,6 +99,7 @@ rule token = parse
  	| "eventually"     { CT_EVENTUALLY }
  	| "everytime"      { CT_EVERYTIME }
 	| "False"          { CT_FALSE }
+	| "forall"         { CT_FORALL }
  	| "happened"       { CT_HAPPENED }
  	| "has"            { CT_HAS }
 	| "if"             { CT_IF }
diff --git a/src/lib/PropertyParser.mly b/src/lib/PropertyParser.mly
index 368c96b4..bf00c136 100644
--- a/src/lib/PropertyParser.mly
+++ b/src/lib/PropertyParser.mly
@@ -60,7 +60,7 @@ let resolve_property l =
 	CT_COVERCARTOGRAPHY
 	CT_DEADLOCKFREE
 	CT_E CT_EF CT_EF_timed CT_EFpmax CT_EFpmin CT_EFtmin CT_EG CT_EVENTUALLY CT_EVERYTIME CT_EXEMPLIFY CT_EXHIBIT
-	CT_FALSE
+	CT_FALSE CT_FORALL
 	CT_HAPPENED CT_HAS
 	CT_IF CT_IMCONVEX CT_IMK CT_IMUNION CT_IN CT_INFCYCLE CT_INFCYCLETHROUGH CT_INFINITY CT_IS
 	CT_LIST CT_LOC
@@ -90,7 +90,7 @@ let resolve_property l =
 
 
 %start main             /* the entry point */
-%type <ParsingStructure.parsed_property> main
+%type <ParsingStructure.unexpanded_parsed_property> main
 %%
 
 /************************************************************/
@@ -111,10 +111,10 @@ quantified_property:
 /************************************************************/
 	synth_or_exhibit property semicolon_opt projection_definition {
 		{
-			synthesis_type	= $1;
-			property		= $2;
+			unexpanded_synthesis_type	= $1;
+			unexpanded_property		= $2;
 			(* Projection *)
-			projection		= $4;
+			unexpanded_projection		= $4;
 		}
 
 	}
@@ -133,44 +133,44 @@ property:
 	/* Basic properties */
 	/*------------------------------------------------------------*/
 	/* Reachability */
-	| CT_VALID { Parsed_Valid }
+	| CT_VALID { Unexpanded_Parsed_Valid }
 
 	/*------------------------------------------------------------*/
 	/* Non-nested CTL */
 	/*------------------------------------------------------------*/
 
 	/* Reachability */
-	| CT_EF state_predicate { Parsed_EF $2 }
+	| CT_EF state_predicate { Unexpanded_Parsed_EF $2 }
 
 	/* Safety */
-	| CT_AGnot state_predicate { Parsed_AGnot $2 }
+	| CT_AGnot state_predicate { Unexpanded_Parsed_AGnot $2 }
 
 	/* Global invariant */
-	| CT_AG state_predicate { Parsed_AG $2 }
+	| CT_AG state_predicate { Unexpanded_Parsed_AG $2 }
 
 	/* Exists globally */
-	| CT_EG state_predicate { Parsed_EG $2 }
+	| CT_EG state_predicate { Unexpanded_Parsed_EG $2 }
 
 	/* Exists release */
-	| CT_E state_predicate CT_R state_predicate { Parsed_ER ($2, $4) }
+	| CT_E state_predicate CT_R state_predicate { Unexpanded_Parsed_ER ($2, $4) }
 
 	/* Exists until */
-	| CT_E state_predicate CT_U state_predicate { Parsed_EU ($2, $4) }
+	| CT_E state_predicate CT_U state_predicate { Unexpanded_Parsed_EU ($2, $4) }
 
 	/* Exists weak until */
-	| CT_E state_predicate CT_W state_predicate { Parsed_EW ($2, $4) }
+	| CT_E state_predicate CT_W state_predicate { Unexpanded_Parsed_EW ($2, $4) }
 
 	/* Unavoidability */
-	| CT_AF state_predicate { Parsed_AF $2 }
+	| CT_AF state_predicate { Unexpanded_Parsed_AF $2 }
 
 	/* Always release */
-	| CT_A state_predicate CT_R state_predicate { Parsed_AR ($2, $4) }
+	| CT_A state_predicate CT_R state_predicate { Unexpanded_Parsed_AR ($2, $4) }
 
 	/* Always until */
-	| CT_A state_predicate CT_U state_predicate { Parsed_AU ($2, $4) }
+	| CT_A state_predicate CT_U state_predicate { Unexpanded_Parsed_AU ($2, $4) }
 
 	/* Always weak until */
-	| CT_A state_predicate CT_W state_predicate { Parsed_AW ($2, $4) }
+	| CT_A state_predicate CT_W state_predicate { Unexpanded_Parsed_AW ($2, $4) }
 
 
 	/*------------------------------------------------------------*/
@@ -181,8 +181,8 @@ property:
 		(* Optimization: `EF_timed [0, infinity) sp` is actually `EF sp` *)
 		match $2 with
 		| Parsed_closed_infinity_interval parsed_interval when parsed_interval = Linear_term (Constant NumConst.zero) ->
-			Parsed_EF $3
-		| _ -> Parsed_EF_timed ($2, $3)
+			Unexpanded_Parsed_EF $3
+		| _ -> Unexpanded_Parsed_EF_timed ($2, $3)
 	}
 
 	/* ER (timed version) */
@@ -190,8 +190,8 @@ property:
 		(* Optimization: `ER_timed [0, infinity) sp sp` is actually `ER sp sp` *)
 		match $4 with
 		| Parsed_closed_infinity_interval parsed_interval when parsed_interval = Linear_term (Constant NumConst.zero) ->
-			Parsed_ER ($2, $5)
-		| _ -> Parsed_ER_timed ($4, $2, $5)
+			Unexpanded_Parsed_ER ($2, $5)
+		| _ -> Unexpanded_Parsed_ER_timed ($4, $2, $5)
 	}
 
 	/* EU (timed version) */
@@ -199,8 +199,8 @@ property:
 		(* Optimization: `EU_timed [0, infinity) sp sp` is actually `EU sp sp` *)
 		match $4 with
 		| Parsed_closed_infinity_interval parsed_interval when parsed_interval = Linear_term (Constant NumConst.zero) ->
-			Parsed_EU ($2, $5)
-		| _ -> Parsed_EU_timed ($4, $2, $5)
+			Unexpanded_Parsed_EU ($2, $5)
+		| _ -> Unexpanded_Parsed_EU_timed ($4, $2, $5)
 	}
 
 	/* EW (timed version) */
@@ -208,8 +208,8 @@ property:
 		(* Optimization: `EW_timed [0, infinity) sp sp` is actually `EW sp sp` *)
 		match $4 with
 		| Parsed_closed_infinity_interval parsed_interval when parsed_interval = Linear_term (Constant NumConst.zero) ->
-			Parsed_EW ($2, $5)
-		| _ -> Parsed_EW_timed ($4, $2, $5)
+			Unexpanded_Parsed_EW ($2, $5)
+		| _ -> Unexpanded_Parsed_EW_timed ($4, $2, $5)
 	}
 
 	/* AF (timed version) */
@@ -217,8 +217,8 @@ property:
 		(* Optimization: `AF_timed [0, infinity) sp` is actually `AF sp` *)
 		match $2 with
 		| Parsed_closed_infinity_interval parsed_interval when parsed_interval = Linear_term (Constant NumConst.zero) ->
-			Parsed_AF $3
-		| _ -> Parsed_AF_timed ($2, $3)
+			Unexpanded_Parsed_AF $3
+		| _ -> Unexpanded_Parsed_AF_timed ($2, $3)
 	}
 
 	/* AR (timed version) */
@@ -226,8 +226,8 @@ property:
 		(* Optimization: `AR_timed [0, infinity) sp sp` is actually `AR sp sp` *)
 		match $4 with
 		| Parsed_closed_infinity_interval parsed_interval when parsed_interval = Linear_term (Constant NumConst.zero) ->
-			Parsed_AR ($2, $5)
-		| _ -> Parsed_AR_timed ($4, $2, $5)
+			Unexpanded_Parsed_AR ($2, $5)
+		| _ -> Unexpanded_Parsed_AR_timed ($4, $2, $5)
 	}
 
 	/* AU (timed version) */
@@ -235,8 +235,8 @@ property:
 		(* Optimization: `AU_timed [0, infinity) sp sp` is actually `AU sp sp` *)
 		match $4 with
 		| Parsed_closed_infinity_interval parsed_interval when parsed_interval = Linear_term (Constant NumConst.zero) ->
-			Parsed_AU ($2, $5)
-		| _ -> Parsed_AU_timed ($4, $2, $5)
+			Unexpanded_Parsed_AU ($2, $5)
+		| _ -> Unexpanded_Parsed_AU_timed ($4, $2, $5)
 	}
 
 	/* AW (timed version) */
@@ -244,8 +244,8 @@ property:
 		(* Optimization: `AW_timed [0, infinity) sp sp` is actually `AW sp sp` *)
 		match $4 with
 		| Parsed_closed_infinity_interval parsed_interval when parsed_interval = Linear_term (Constant NumConst.zero) ->
-			Parsed_AW ($2, $5)
-		| _ -> Parsed_AW_timed ($4, $2, $5)
+			Unexpanded_Parsed_AW ($2, $5)
+		| _ -> Unexpanded_Parsed_AW_timed ($4, $2, $5)
 	}
 
 
@@ -255,15 +255,15 @@ property:
 	/*------------------------------------------------------------*/
 
 	/* Reachability with minimization of a parameter valuation */
-	| CT_EFpmin state_predicate COMMA NAME { Parsed_EFpmin ($2, $4) }
-	| CT_EFpmin LPAREN state_predicate COMMA NAME RPAREN { Parsed_EFpmin ($3, $5) }
+	| CT_EFpmin state_predicate COMMA NAME { Unexpanded_Parsed_EFpmin ($2, $4) }
+	| CT_EFpmin LPAREN state_predicate COMMA NAME RPAREN { Unexpanded_Parsed_EFpmin ($3, $5) }
 
 	/* Reachability with maximization of a parameter valuation */
-	| CT_EFpmax state_predicate COMMA NAME { Parsed_EFpmax ($2, $4) }
-	| CT_EFpmax LPAREN state_predicate COMMA NAME RPAREN { Parsed_EFpmax ($3, $5) }
+	| CT_EFpmax state_predicate COMMA NAME { Unexpanded_Parsed_EFpmax ($2, $4) }
+	| CT_EFpmax LPAREN state_predicate COMMA NAME RPAREN { Unexpanded_Parsed_EFpmax ($3, $5) }
 
 	/* Reachability with minimal-time */
-	| CT_EFtmin state_predicate { Parsed_EFtmin ($2) }
+	| CT_EFtmin state_predicate { Unexpanded_Parsed_EFtmin ($2) }
 
 
 	/*------------------------------------------------------------*/
@@ -271,22 +271,22 @@ property:
 	/*------------------------------------------------------------*/
 
 	/* Infinite-run (cycle) */
-	| CT_INFCYCLE { Parsed_Cycle_Through (Parsed_state_predicate_term (Parsed_state_predicate_factor(Parsed_simple_predicate Parsed_state_predicate_true))) }
+	| CT_INFCYCLE { Unexpanded_Parsed_Cycle_Through (Unexpanded_Parsed_state_predicate_term (Unexpanded_Parsed_state_predicate_factor(Unexpanded_Parsed_simple_predicate Unexpanded_Parsed_state_predicate_true))) }
 
 	/* Accepting infinite-run (cycle) through a state predicate */
 	| CT_INFCYCLETHROUGH LPAREN state_predicate_list RPAREN {
 		(* Check whether the list is of size <= 1 *)
 		match $3 with
-		| []				-> Parsed_Cycle_Through (Parsed_state_predicate_term (Parsed_state_predicate_factor(Parsed_simple_predicate Parsed_state_predicate_false))) (* NOTE: equivalent to False; this case probably cannot happen anyway *)
-		| [state_predicate]	-> Parsed_Cycle_Through state_predicate
-		| _					-> Parsed_Cycle_Through_generalized $3
+		| []				-> Unexpanded_Parsed_Cycle_Through (Unexpanded_Parsed_state_predicate_term (Unexpanded_Parsed_state_predicate_factor(Unexpanded_Parsed_simple_predicate Unexpanded_Parsed_state_predicate_false))) (* NOTE: equivalent to False; this case probably cannot happen anyway *)
+		| [state_predicate]	-> Unexpanded_Parsed_Cycle_Through state_predicate
+		| _					-> Unexpanded_Parsed_Cycle_Through_generalized $3
 		}
 
 	/* Accepting infinite-run (cycle) through accepting locations */
-	| CT_ACCEPTINGCYCLE { Parsed_Cycle_Through (Parsed_state_predicate_term (Parsed_state_predicate_factor(Parsed_simple_predicate Parsed_state_predicate_accepting))) }
+	| CT_ACCEPTINGCYCLE { Unexpanded_Parsed_Cycle_Through (Unexpanded_Parsed_state_predicate_term (Unexpanded_Parsed_state_predicate_factor(Unexpanded_Parsed_simple_predicate Unexpanded_Parsed_state_predicate_accepting))) }
 
 	/* Infinite-run (cycle) with non-Zeno assumption */
-	| CT_NZCYCLE { Parsed_NZ_Cycle }
+	| CT_NZCYCLE { Unexpanded_Parsed_NZ_Cycle }
 
 
 	/*------------------------------------------------------------*/
@@ -294,22 +294,22 @@ property:
 	/*------------------------------------------------------------*/
 
 	/* Deadlock-free synthesis */
-	| CT_DEADLOCKFREE { Parsed_Deadlock_Freeness }
+	| CT_DEADLOCKFREE { Unexpanded_Parsed_Deadlock_Freeness }
 
 
 	/*------------------------------------------------------------*/
 	/* Inverse method, trace preservation, robustness */
 	/*------------------------------------------------------------*/
 
-	| CT_TRACEPRESERVATION LPAREN reference_valuation RPAREN { Parsed_IM $3 }
+	| CT_TRACEPRESERVATION LPAREN reference_valuation RPAREN { Unexpanded_Parsed_IM $3 }
 
-	| CT_IMCONVEX LPAREN reference_valuation RPAREN { Parsed_ConvexIM $3 }
+	| CT_IMCONVEX LPAREN reference_valuation RPAREN { Unexpanded_Parsed_ConvexIM $3 }
 
-	| CT_PRP LPAREN state_predicate COMMA reference_valuation RPAREN { Parsed_PRP ($3 , $5) }
+	| CT_PRP LPAREN state_predicate COMMA reference_valuation RPAREN { Unexpanded_Parsed_PRP ($3 , $5) }
 
-	| CT_IMK LPAREN reference_valuation RPAREN { Parsed_IMK $3 }
+	| CT_IMK LPAREN reference_valuation RPAREN { Unexpanded_Parsed_IMK $3 }
 
-	| CT_IMUNION LPAREN reference_valuation RPAREN { Parsed_IMunion $3 }
+	| CT_IMUNION LPAREN reference_valuation RPAREN { Unexpanded_Parsed_IMunion $3 }
 
 
 	/*------------------------------------------------------------*/
@@ -317,37 +317,37 @@ property:
 	/*------------------------------------------------------------*/
 
 	/* Cartography */
-	| CT_COVERCARTOGRAPHY LPAREN reference_rectangle RPAREN { Parsed_Cover_cartography ($3 , Constants.default_cartography_step) }
-	| CT_COVERCARTOGRAPHY LPAREN reference_rectangle COMMA CT_STEP OP_EQ rational RPAREN { Parsed_Cover_cartography ($3 , $7) }
+	| CT_COVERCARTOGRAPHY LPAREN reference_rectangle RPAREN { Unexpanded_Parsed_Cover_cartography ($3 , Constants.default_cartography_step) }
+	| CT_COVERCARTOGRAPHY LPAREN reference_rectangle COMMA CT_STEP OP_EQ rational RPAREN { Unexpanded_Parsed_Cover_cartography ($3 , $7) }
 
-	| CT_BCLEARN LPAREN state_predicate COMMA reference_rectangle RPAREN { Parsed_Learning_cartography ($3, $5, Constants.default_cartography_step) }
-	| CT_BCLEARN LPAREN state_predicate COMMA reference_rectangle COMMA CT_STEP OP_EQ rational RPAREN { Parsed_Learning_cartography ($3, $5, $9) }
+	| CT_BCLEARN LPAREN state_predicate COMMA reference_rectangle RPAREN { Unexpanded_Parsed_Learning_cartography ($3, $5, Constants.default_cartography_step) }
+	| CT_BCLEARN LPAREN state_predicate COMMA reference_rectangle COMMA CT_STEP OP_EQ rational RPAREN { Unexpanded_Parsed_Learning_cartography ($3, $5, $9) }
 
-	| CT_BCSHUFFLE LPAREN reference_rectangle RPAREN { Parsed_Shuffle_cartography ($3, Constants.default_cartography_step) }
-	| CT_BCSHUFFLE LPAREN reference_rectangle COMMA CT_STEP OP_EQ rational RPAREN { Parsed_Shuffle_cartography ($3, $7) }
+	| CT_BCSHUFFLE LPAREN reference_rectangle RPAREN { Unexpanded_Parsed_Shuffle_cartography ($3, Constants.default_cartography_step) }
+	| CT_BCSHUFFLE LPAREN reference_rectangle COMMA CT_STEP OP_EQ rational RPAREN { Unexpanded_Parsed_Shuffle_cartography ($3, $7) }
 
-	| CT_BCBORDER LPAREN reference_rectangle RPAREN { Parsed_Border_cartography ($3, Constants.default_cartography_step) }
-	| CT_BCBORDER LPAREN reference_rectangle COMMA CT_STEP OP_EQ rational RPAREN { Parsed_Border_cartography ($3, $7) }
+	| CT_BCBORDER LPAREN reference_rectangle RPAREN { Unexpanded_Parsed_Border_cartography ($3, Constants.default_cartography_step) }
+	| CT_BCBORDER LPAREN reference_rectangle COMMA CT_STEP OP_EQ rational RPAREN { Unexpanded_Parsed_Border_cartography ($3, $7) }
 
-	| CT_BCRANDOM LPAREN reference_rectangle COMMA pos_integer RPAREN { Parsed_Random_cartography ($3, $5, Constants.default_cartography_step) }
-	| CT_BCRANDOM LPAREN reference_rectangle COMMA pos_integer COMMA CT_STEP OP_EQ rational RPAREN { Parsed_Random_cartography ($3, $5, $9) }
+	| CT_BCRANDOM LPAREN reference_rectangle COMMA pos_integer RPAREN { Unexpanded_Parsed_Random_cartography ($3, $5, Constants.default_cartography_step) }
+	| CT_BCRANDOM LPAREN reference_rectangle COMMA pos_integer COMMA CT_STEP OP_EQ rational RPAREN { Unexpanded_Parsed_Random_cartography ($3, $5, $9) }
 
-	| CT_BCRANDOMSEQ LPAREN reference_rectangle COMMA pos_integer RPAREN { Parsed_RandomSeq_cartography ($3, $5, Constants.default_cartography_step) }
-	| CT_BCRANDOMSEQ LPAREN reference_rectangle COMMA pos_integer COMMA CT_STEP OP_EQ rational RPAREN { Parsed_RandomSeq_cartography ($3, $5, $9) }
+	| CT_BCRANDOMSEQ LPAREN reference_rectangle COMMA pos_integer RPAREN { Unexpanded_Parsed_RandomSeq_cartography ($3, $5, Constants.default_cartography_step) }
+	| CT_BCRANDOMSEQ LPAREN reference_rectangle COMMA pos_integer COMMA CT_STEP OP_EQ rational RPAREN { Unexpanded_Parsed_RandomSeq_cartography ($3, $5, $9) }
 
-	| CT_PRPC LPAREN state_predicate COMMA reference_rectangle RPAREN { Parsed_PRPC ($3,$5, Constants.default_cartography_step) }
-	| CT_PRPC LPAREN state_predicate COMMA reference_rectangle COMMA CT_STEP OP_EQ rational RPAREN { Parsed_PRPC ($3,$5, $9) }
+	| CT_PRPC LPAREN state_predicate COMMA reference_rectangle RPAREN { Unexpanded_Parsed_PRPC ($3,$5, Constants.default_cartography_step) }
+	| CT_PRPC LPAREN state_predicate COMMA reference_rectangle COMMA CT_STEP OP_EQ rational RPAREN { Unexpanded_Parsed_PRPC ($3,$5, $9) }
 
 
 	/*------------------------------------------------------------*/
 	/* Observer patterns */
 	/*------------------------------------------------------------*/
-	| CT_PATTERN LPAREN pattern RPAREN { Parsed_pattern ($3) }
+	| CT_PATTERN LPAREN pattern RPAREN { Unexpanded_Parsed_pattern ($3) }
 
 	/*------------------------------------------------------------*/
 	/* Observer patterns */
 	/*------------------------------------------------------------*/
-	| CT_WIN state_predicate { Parsed_Win ($2) }
+	| CT_WIN state_predicate { Unexpanded_Parsed_Win ($2) }
 
 ;
 
@@ -422,7 +422,7 @@ state_predicate_list:
 /************************************************************/
 	| non_empty_state_predicate_list { $1 }
 	/* Also allow empty state predicate, equivalent to False */
-	| { [Parsed_state_predicate_term (Parsed_state_predicate_factor(Parsed_simple_predicate Parsed_state_predicate_false))] }
+	| { [Unexpanded_Parsed_state_predicate_term (Unexpanded_Parsed_state_predicate_factor(Unexpanded_Parsed_simple_predicate Unexpanded_Parsed_state_predicate_false))] }
 ;
 
 /************************************************************/
@@ -437,51 +437,60 @@ state_predicate:
 /************************************************************/
 	| non_empty_state_predicate { $1 }
 	/* Also allow empty state predicate, equivalent to False */
-	| { Parsed_state_predicate_term (Parsed_state_predicate_factor(Parsed_simple_predicate Parsed_state_predicate_false)) }
+	| { Unexpanded_Parsed_state_predicate_term (Unexpanded_Parsed_state_predicate_factor(Unexpanded_Parsed_simple_predicate Unexpanded_Parsed_state_predicate_false)) }
 ;
 
 /************************************************************/
 non_empty_state_predicate:
 /************************************************************/
-	| non_empty_state_predicate OP_DISJUNCTION state_predicate_term { Parsed_state_predicate_OR ($1, Parsed_state_predicate_term $3) }
+	| non_empty_state_predicate OP_DISJUNCTION state_predicate_term { Unexpanded_Parsed_state_predicate_OR ($1, Unexpanded_Parsed_state_predicate_term $3) }
 
 	/* Translate 'a => b' to 'NOT a OR b' */
-	| non_empty_state_predicate OP_IMPLIES state_predicate_term { Parsed_state_predicate_OR (Parsed_state_predicate_term (Parsed_state_predicate_factor (Parsed_state_predicate_factor_NOT (Parsed_state_predicate ($1)))), Parsed_state_predicate_term $3) }
+	| non_empty_state_predicate OP_IMPLIES state_predicate_term { Unexpanded_Parsed_state_predicate_OR (Unexpanded_Parsed_state_predicate_term (Unexpanded_Parsed_state_predicate_factor (Unexpanded_Parsed_state_predicate_factor_NOT (Unexpanded_Parsed_state_predicate ($1)))), Unexpanded_Parsed_state_predicate_term $3) }
 
-	| state_predicate_term { Parsed_state_predicate_term $1 }
+	| state_predicate_term { Unexpanded_Parsed_state_predicate_term $1 }
 ;
 
 state_predicate_term:
-	| state_predicate_term OP_CONJUNCTION state_predicate_factor { Parsed_state_predicate_term_AND ($1, Parsed_state_predicate_factor $3) }
-	| state_predicate_factor { Parsed_state_predicate_factor $1 }
+	| state_predicate_term OP_CONJUNCTION state_predicate_factor { Unexpanded_Parsed_state_predicate_term_AND ($1, Unexpanded_Parsed_state_predicate_factor $3) }
+	| state_predicate_factor { Unexpanded_Parsed_state_predicate_factor $1 }
 ;
 
 state_predicate_factor:
-	| simple_predicate { Parsed_simple_predicate $1 }
-	| CT_NOT state_predicate_factor { Parsed_state_predicate_factor_NOT $2 }
-	| LPAREN non_empty_state_predicate RPAREN { Parsed_state_predicate $2 }
+	| simple_predicate { Unexpanded_Parsed_simple_predicate $1 }
+	| CT_NOT state_predicate_factor { Unexpanded_Parsed_state_predicate_factor_NOT $2 }
+	| LPAREN non_empty_state_predicate RPAREN { Unexpanded_Parsed_state_predicate $2 }
+	| forall_common_prefix simple_predicate { Unexpanded_Parsed_forall_simple_predicate ($1, $2) }
+	| forall_common_prefix LPAREN non_empty_state_predicate RPAREN { Unexpanded_Parsed_forall_state_predicate ($1, $3) }
+
 ;
 
 /* A single definition of one bad location or one bad discrete definition */
 simple_predicate:
-	| discrete_boolean_predicate { Parsed_discrete_boolean_expression($1) }
-	| loc_predicate { Parsed_loc_predicate ($1) }
-	| CT_ACCEPTING { Parsed_state_predicate_accepting }
+	| discrete_boolean_predicate { Unexpanded_Parsed_discrete_boolean_expression($1) }
+	| loc_predicate { Unexpanded_Parsed_loc_predicate ($1) }
+	| CT_ACCEPTING { Unexpanded_Parsed_state_predicate_accepting }
 ;
 
+/************************************************************/
+name_or_array_access:
+  | NAME { Var_name $1 }
+  | NAME LSQBRA arithmetic_expression RSQBRA { Var_array_access ($1, $3) }
+;
+/************************************************************/
 
 /************************************************************/
 loc_predicate:
 /************************************************************/
 	/* loc[my_pta] = my_loc */
-	| CT_LOC LSQBRA NAME RSQBRA OP_EQ NAME { Parsed_loc_predicate_EQ ($3, $6) }
+	| CT_LOC LSQBRA name_or_array_access RSQBRA OP_EQ NAME { Unexpanded_Parsed_loc_predicate_EQ ($3, $6) }
 	/* my_pta IS IN my_loc */
-	| NAME CT_IS CT_IN NAME { Parsed_loc_predicate_EQ ($1, $4) }
+	| name_or_array_access CT_IS CT_IN NAME { Unexpanded_Parsed_loc_predicate_EQ ($1, $4) }
 
 	/* loc[my_pta] <> my_loc */
-	| CT_LOC LSQBRA NAME RSQBRA OP_NEQ NAME { Parsed_loc_predicate_NEQ ($3, $6) }
+	| CT_LOC LSQBRA name_or_array_access RSQBRA OP_NEQ NAME { Unexpanded_Parsed_loc_predicate_NEQ ($3, $6) }
 	/* my_pta IS NOT IN my_loc */
-	| NAME CT_IS CT_NOT CT_IN NAME { Parsed_loc_predicate_EQ ($1, $5) }
+	| name_or_array_access CT_IS CT_NOT CT_IN NAME { Unexpanded_Parsed_loc_predicate_NEQ ($1, $5) }
 ;
 
 
@@ -790,3 +799,13 @@ semicolon_opt:
 	| SEMICOLON { }
 	| { }
 ;
+
+/************************************************************/
+/** MISC. */
+/************************************************************/
+
+forall_common_prefix:
+  | CT_FORALL NAME CT_IN LSQBRA arithmetic_expression COMMA arithmetic_expression RSQBRA COLON
+  {
+    { forall_index_name = $2; forall_lb = $5; forall_ub = $7}
+  }
diff --git a/src/lib/Templates.ml b/src/lib/Templates.ml
index 9e7d228b..3ab3f171 100644
--- a/src/lib/Templates.ml
+++ b/src/lib/Templates.ml
@@ -126,6 +126,9 @@ let indices_from_forall_index_data g_decls forall_index_data =
   let forall_ub_val = eval_parsed_arithmetic_expr g_decls forall_ub |> NumConst.to_bounded_int in
   List.init (forall_ub_val - forall_lb_val + 1) (fun i -> i + forall_lb_val)
 
+let gen_aux_var_tbl i index_data =
+  Hashtbl.of_seq (List.to_seq [(index_data.forall_index_name, Arg_int (NumConst.numconst_of_int i))])
+
 (*****************************************************************************)
 (* Instantiation of templates *)
 (*****************************************************************************)
@@ -456,7 +459,8 @@ let expand_synt_arrays_automaton (g_decls : variable_declarations) (synt_vars :
 let expand_synt_arrays_automata (g_decls : variable_declarations) (synt_vars : synt_vars_data) : unexpanded_parsed_automaton list -> parsed_automaton list =
   List.map (expand_synt_arrays_automaton g_decls synt_vars)
 
-let expand_forall_call g_decls { forall_index_data; forall_template; forall_aut_name; forall_args } =
+let expand_forall_call (g_decls: variable_declarations) (call_data: parsed_forall_template_call) =
+  let { forall_index_data; forall_template; forall_aut_name; forall_args } = call_data in
   let indices = indices_from_forall_index_data g_decls forall_index_data in
   let instantiate_arg idx = fun arg ->
     match arg with
@@ -473,10 +477,7 @@ let expand_forall_call g_decls { forall_index_data; forall_template; forall_aut_
   in
   List.map build_call indices
 
-let expand_init_state_predicate g_decls pred =
-  let gen_aux_var_tbl i index_data =
-    Hashtbl.of_seq (List.to_seq [(index_data.forall_index_name, Arg_int (NumConst.numconst_of_int i))])
-  in
+let expand_init_state_predicate (g_decls: variable_declarations) (pred: unexpanded_parsed_init_state_predicate): parsed_init_state_predicate list =
   match pred with
     | Unexpanded_parsed_forall_loc_assignment (index_data, arr_name, arr_idx, loc_name) ->
         let instantiate_arr_idx i arr_idx =
@@ -502,30 +503,31 @@ let expand_init_state_predicate g_decls pred =
     | Unexpanded_parsed_discrete_predicate (name, bool_expr) ->
         [Parsed_discrete_predicate (name, bool_expr)]
 
-let expand_init_definition g_decls = List.concat_map (expand_init_state_predicate g_decls)
+let expand_init_definition (g_decls: variable_declarations): unexpanded_parsed_init_state_predicate list -> parsed_init_state_predicate list =
+  List.concat_map (expand_init_state_predicate g_decls)
 
-let expand_model (unexpanded_parsed_model : unexpanded_parsed_model) : parsed_model =
-  let g_decls = unexpanded_parsed_model.unexpanded_variable_declarations in
+let expand_model (model : unexpanded_parsed_model) : parsed_model =
+  let g_decls = model.unexpanded_variable_declarations in
 
   (* Expand foralls *)
   let forall_calls =
-    unexpanded_parsed_model.forall_template_calls |>
+    model.forall_template_calls |>
     List.concat_map (expand_forall_call g_decls)
   in
-  let all_calls = unexpanded_parsed_model.template_calls @ forall_calls in
-  let instantiated_automata = instantiate_automata unexpanded_parsed_model.template_definitions all_calls in
-  let all_automata = unexpanded_parsed_model.unexpanded_automata @ instantiated_automata in
+  let all_calls = model.template_calls @ forall_calls in
+  let instantiated_automata = instantiate_automata model.template_definitions all_calls in
+  let all_automata = model.unexpanded_automata @ instantiated_automata in
 
   let synt_vars =
     List.concat_map
       (fun ((len, kind), names) -> List.map (fun name -> (name, kind, NumConst.to_bounded_int (eval_parsed_arithmetic_expr g_decls len))) names)
-      unexpanded_parsed_model.synt_declarations
+      model.synt_declarations
   in
   (* NOTE: at this point `parsed_action` calls must have an integer as argument, not an arbitrary expression *)
   let expanded_automata = expand_synt_arrays_automata g_decls synt_vars all_automata in
   let expanded_decls = expand_synt_decls synt_vars in
   let expanded_controllable_actions =
-    match unexpanded_parsed_model.unexpanded_controllable_actions with
+    match model.unexpanded_controllable_actions with
       | Unexpanded_parsed_controllable_actions actions ->
           Parsed_controllable_actions (expand_name_or_access_list g_decls actions)
       | Unexpanded_parsed_uncontrollable_actions actions ->
@@ -534,12 +536,206 @@ let expand_model (unexpanded_parsed_model : unexpanded_parsed_model) : parsed_mo
   in
 
   let expanded_init_definition =
-    expand_init_definition g_decls unexpanded_parsed_model.unexpanded_init_definition
+    expand_init_definition g_decls model.unexpanded_init_definition
   in
 
   { controllable_actions  = expanded_controllable_actions;
-    variable_declarations = unexpanded_parsed_model.unexpanded_variable_declarations @ expanded_decls;
-    fun_definitions       = unexpanded_parsed_model.unexpanded_fun_definitions;
+    variable_declarations = model.unexpanded_variable_declarations @ expanded_decls;
+    fun_definitions       = model.unexpanded_fun_definitions;
     automata              = expanded_automata;
     init_definition       = expanded_init_definition;
   }
+
+let instantiate_name_or_access (param_map: var_map) (aut: name_or_access): name_or_access =
+  match aut with
+    | Var_name _ -> aut
+    | Var_array_access (arr, idx) ->
+        let instantiated_idx = instantiate_discrete_arithmetic_expression param_map idx in
+        Var_array_access (arr, instantiated_idx)
+
+let instantiate_simple_predicate (param_map: var_map) (spred: unexpanded_parsed_simple_predicate): unexpanded_parsed_simple_predicate =
+  match spred with
+    | Unexpanded_Parsed_discrete_boolean_expression expr ->
+        Unexpanded_Parsed_discrete_boolean_expression (instantiate_discrete_boolean_expression param_map expr)
+    | Unexpanded_Parsed_loc_predicate (Unexpanded_Parsed_loc_predicate_EQ (aut, loc)) ->
+        let instantiated_aut = instantiate_name_or_access param_map aut in
+        Unexpanded_Parsed_loc_predicate (Unexpanded_Parsed_loc_predicate_EQ (instantiated_aut, loc))
+    | Unexpanded_Parsed_loc_predicate (Unexpanded_Parsed_loc_predicate_NEQ (aut, loc)) ->
+        let instantiated_aut = instantiate_name_or_access param_map aut in
+        Unexpanded_Parsed_loc_predicate (Unexpanded_Parsed_loc_predicate_NEQ (instantiated_aut, loc))
+    | _ -> spred
+
+let rec instantiate_state_predicate (param_map: var_map): unexpanded_parsed_state_predicate -> unexpanded_parsed_state_predicate = function
+  | Unexpanded_Parsed_state_predicate_OR (pred1, pred2) ->
+      let instantiated_pred1 = instantiate_state_predicate param_map pred1 in
+      let instantiated_pred2 = instantiate_state_predicate param_map pred2 in
+      Unexpanded_Parsed_state_predicate_OR (instantiated_pred1, instantiated_pred2)
+  | Unexpanded_Parsed_state_predicate_term t ->
+      Unexpanded_Parsed_state_predicate_term (instantiate_state_term param_map t)
+
+and instantiate_state_term (param_map: var_map): unexpanded_parsed_state_predicate_term -> unexpanded_parsed_state_predicate_term = function
+  | Unexpanded_Parsed_state_predicate_term_AND (t1, t2) ->
+      let instantiated_t1 = instantiate_state_term param_map t1 in
+      let instantiated_t2 = instantiate_state_term param_map t2 in
+      Unexpanded_Parsed_state_predicate_term_AND (instantiated_t1, instantiated_t2)
+  | Unexpanded_Parsed_state_predicate_factor f ->
+      Unexpanded_Parsed_state_predicate_factor (instantiate_state_factor param_map f)
+  (* TODO: Refactor the next two branches *)
+and instantiate_state_factor (param_map: var_map): unexpanded_parsed_state_predicate_factor -> unexpanded_parsed_state_predicate_factor = function
+  | Unexpanded_Parsed_state_predicate_factor_NOT f -> Unexpanded_Parsed_state_predicate_factor_NOT (instantiate_state_factor param_map f)
+  | Unexpanded_Parsed_simple_predicate spred -> Unexpanded_Parsed_simple_predicate (instantiate_simple_predicate param_map spred)
+  | Unexpanded_Parsed_state_predicate pred -> Unexpanded_Parsed_state_predicate (instantiate_state_predicate param_map pred)
+  | Unexpanded_Parsed_forall_state_predicate (index_data, pred) ->
+      let binded_name = index_data.forall_index_name in
+      let prev_binded_value_opt = Hashtbl.find_opt param_map binded_name in
+      (* Here we remove the binde to allow the inner forall to rebind it. *)
+      (* This means that if the user had something like `forall i in [0, 1]: forall i in [0, 1]: (p(i)) && q(i)`, the inner one will be
+         substituted first, and the outer one will substitute only `q(i)` *)
+      Hashtbl.remove param_map binded_name;
+      let r = Unexpanded_Parsed_forall_state_predicate (index_data, instantiate_state_predicate param_map pred) in
+      begin match prev_binded_value_opt with
+        | Some v -> Hashtbl.add param_map binded_name v; r
+        | None -> r
+      end
+  | Unexpanded_Parsed_forall_simple_predicate (index_data, spred) ->
+      let binded_name = index_data.forall_index_name in
+      let prev_binded_value_opt = Hashtbl.find_opt param_map binded_name in
+      (* Here we remove the binde to allow the inner forall to rebind it. *)
+      (* This means that if the user had something like `forall i in [0, 1]: (forall i in [0, 1]: (p(i)) && q(i))`, the inner one will be
+         substituted first, and the outer one will substitute only `q(i)` *)
+      Hashtbl.remove param_map binded_name;
+      let r = Unexpanded_Parsed_forall_simple_predicate (index_data, instantiate_simple_predicate param_map spred) in
+      begin match prev_binded_value_opt with
+        | Some v -> Hashtbl.add param_map binded_name v; r
+        | None -> r
+      end
+
+let expand_loc_pred (g_decls: variable_declarations): unexpanded_parsed_loc_predicate -> parsed_loc_predicate = function
+  | Unexpanded_Parsed_loc_predicate_EQ (aut_name, loc) -> Parsed_loc_predicate_EQ (expand_name_or_access g_decls aut_name, loc)
+  | Unexpanded_Parsed_loc_predicate_NEQ (aut_name, loc) -> Parsed_loc_predicate_NEQ (expand_name_or_access g_decls aut_name, loc)
+
+let expand_simple_predicate (g_decls: variable_declarations): unexpanded_parsed_simple_predicate -> parsed_simple_predicate = function
+  | Unexpanded_Parsed_discrete_boolean_expression expr -> Parsed_discrete_boolean_expression expr
+  | Unexpanded_Parsed_loc_predicate loc_pred -> Parsed_loc_predicate (expand_loc_pred g_decls loc_pred)
+  | Unexpanded_Parsed_state_predicate_true -> Parsed_state_predicate_true
+  | Unexpanded_Parsed_state_predicate_false -> Parsed_state_predicate_false
+  | Unexpanded_Parsed_state_predicate_accepting -> Parsed_state_predicate_accepting
+
+let rec expand_state_predicate (g_decls: variable_declarations): unexpanded_parsed_state_predicate -> parsed_state_predicate = function
+  | Unexpanded_Parsed_state_predicate_OR (pred1, pred2) ->
+      Parsed_state_predicate_OR (expand_state_predicate g_decls pred1, expand_state_predicate g_decls pred2)
+  | Unexpanded_Parsed_state_predicate_term t -> Parsed_state_predicate_term (expand_state_term g_decls t)
+
+and expand_state_term (g_decls: variable_declarations): unexpanded_parsed_state_predicate_term -> parsed_state_predicate_term = function
+  | Unexpanded_Parsed_state_predicate_term_AND (t1, t2) ->
+      Parsed_state_predicate_term_AND (expand_state_term g_decls t1, expand_state_term g_decls t2)
+  | Unexpanded_Parsed_state_predicate_factor f -> Parsed_state_predicate_factor (expand_state_factor g_decls f)
+
+and expand_state_factor (g_decls: variable_declarations) (factor: unexpanded_parsed_state_predicate_factor): parsed_state_predicate_factor =
+  match factor with
+  (* TODO: Refactor the next two branches *)
+  | Unexpanded_Parsed_forall_simple_predicate (index_data, spred) -> begin
+      let indices = indices_from_forall_index_data g_decls index_data in
+      (* Here we reverse the list to preserve the order of the index after the fold *)
+      match List.rev indices with
+      | [] -> failwith "error or vacuity?"
+      | i :: is ->
+            (* Compute the conjunction of spred instantiated with each idx in (i::is) *)
+            let instantiate_spred_with idx =
+              let param_map_idx = gen_aux_var_tbl idx index_data in
+              instantiate_simple_predicate param_map_idx spred |>
+              expand_simple_predicate g_decls
+            in
+            let term_of_simple_pred p = Parsed_state_predicate_factor (Parsed_simple_predicate p) in
+            let spred_i = instantiate_spred_with i in
+            let fold_fun acc idx =
+                let spred_idx = instantiate_spred_with idx in
+                let spred_idx_term = term_of_simple_pred spred_idx in
+                match acc with
+                  | Parsed_state_predicate (Parsed_state_predicate_term t) ->
+                      Parsed_state_predicate (Parsed_state_predicate_term (Parsed_state_predicate_term_AND (spred_idx_term, t)))
+                  | Parsed_simple_predicate p -> (* Only first iteration of fold, after that I know for sure is a term *)
+                      let p_term = term_of_simple_pred p in
+                      Parsed_state_predicate (Parsed_state_predicate_term (Parsed_state_predicate_term_AND (spred_idx_term, p_term)))
+                  | _ -> failwith "[expand_state_factor]: unreachable"
+                in
+            List.fold_left fold_fun (Parsed_simple_predicate spred_i) is
+  end
+  | Unexpanded_Parsed_forall_state_predicate (index_data, pred) -> begin
+      let indices = indices_from_forall_index_data g_decls index_data in
+      match List.rev indices with
+        | [] -> failwith "error or vacuity?"
+        | i :: is ->
+            let instantiate_pred_with idx =
+              let param_map_idx = gen_aux_var_tbl idx index_data in
+              instantiate_state_predicate param_map_idx pred |>
+              expand_state_predicate g_decls
+            in
+            let pred_i = instantiate_pred_with i in
+            let term_of_state_pred p = Parsed_state_predicate_factor (Parsed_state_predicate p) in
+            let fold_fun acc idx =
+              let pred_idx = instantiate_pred_with idx in
+              let pred_idx_term = term_of_state_pred pred_idx in
+              match acc with
+                | Parsed_state_predicate (Parsed_state_predicate_term t) ->
+                    Parsed_state_predicate (Parsed_state_predicate_term (Parsed_state_predicate_term_AND (pred_idx_term, t)))
+                | Parsed_state_predicate p -> (* Only first iteration of fold, after that I know for sure is an and *)
+                    let p_term = term_of_state_pred p in
+                    Parsed_state_predicate (Parsed_state_predicate_term (Parsed_state_predicate_term_AND (pred_idx_term, p_term)))
+                | _ -> failwith "[expand_state_factor]: unreachable"
+            in
+            List.fold_left fold_fun (Parsed_state_predicate pred_i) is
+  end
+  | Unexpanded_Parsed_state_predicate_factor_NOT f -> Parsed_state_predicate_factor_NOT (expand_state_factor g_decls f)
+  | Unexpanded_Parsed_simple_predicate spred -> Parsed_simple_predicate (expand_simple_predicate g_decls spred)
+  | Unexpanded_Parsed_state_predicate pred -> Parsed_state_predicate (expand_state_predicate g_decls pred)
+
+
+let expand_property_type (g_decls: variable_declarations) : unexpanded_parsed_property_type -> parsed_property_type = function
+  | Unexpanded_Parsed_Valid -> Parsed_Valid
+  | Unexpanded_Parsed_EF pred1 -> Parsed_EF (expand_state_predicate g_decls pred1)
+  | Unexpanded_Parsed_AGnot pred1 -> Parsed_AGnot (expand_state_predicate g_decls pred1)
+  | Unexpanded_Parsed_AG pred1 -> Parsed_AG (expand_state_predicate g_decls pred1)
+  | Unexpanded_Parsed_EG pred1 -> Parsed_EG (expand_state_predicate g_decls pred1)
+  | Unexpanded_Parsed_ER (pred1, pred2) -> Parsed_ER (expand_state_predicate g_decls pred1, expand_state_predicate g_decls pred2)
+  | Unexpanded_Parsed_EU (pred1, pred2) -> Parsed_EU (expand_state_predicate g_decls pred1, expand_state_predicate g_decls pred2)
+  | Unexpanded_Parsed_EW (pred1, pred2) -> Parsed_EW (expand_state_predicate g_decls pred1, expand_state_predicate g_decls pred2)
+  | Unexpanded_Parsed_AF pred1 -> Parsed_AF (expand_state_predicate g_decls pred1)
+  | Unexpanded_Parsed_AR (pred1, pred2) -> Parsed_AR (expand_state_predicate g_decls pred1, expand_state_predicate g_decls pred2)
+  | Unexpanded_Parsed_AU (pred1, pred2) -> Parsed_AU (expand_state_predicate g_decls pred1, expand_state_predicate g_decls pred2)
+  | Unexpanded_Parsed_AW (pred1, pred2) -> Parsed_AW (expand_state_predicate g_decls pred1, expand_state_predicate g_decls pred2)
+  | Unexpanded_Parsed_EF_timed (inter, pred1) -> Parsed_EF_timed (inter, expand_state_predicate g_decls pred1)
+  | Unexpanded_Parsed_ER_timed (inter, pred1, pred2) -> Parsed_ER_timed (inter, expand_state_predicate g_decls pred1, expand_state_predicate g_decls pred2)
+  | Unexpanded_Parsed_EU_timed (inter, pred1, pred2) -> Parsed_EU_timed (inter, expand_state_predicate g_decls pred1, expand_state_predicate g_decls pred2)
+  | Unexpanded_Parsed_EW_timed (inter, pred1, pred2) -> Parsed_EW_timed (inter, expand_state_predicate g_decls pred1, expand_state_predicate g_decls pred2)
+  | Unexpanded_Parsed_AF_timed (inter, pred1) -> Parsed_AF_timed (inter, expand_state_predicate g_decls pred1)
+  | Unexpanded_Parsed_AR_timed (inter, pred1, pred2) -> Parsed_AR_timed (inter, expand_state_predicate g_decls pred1, expand_state_predicate g_decls pred2)
+  | Unexpanded_Parsed_AU_timed (inter, pred1, pred2) -> Parsed_AU_timed (inter, expand_state_predicate g_decls pred1, expand_state_predicate g_decls pred2)
+  | Unexpanded_Parsed_AW_timed (inter, pred1, pred2) -> Parsed_AW_timed (inter, expand_state_predicate g_decls pred1, expand_state_predicate g_decls pred2)
+  | Unexpanded_Parsed_EFpmin (pred1, name) -> Parsed_EFpmin (expand_state_predicate g_decls pred1, name)
+  | Unexpanded_Parsed_EFpmax (pred1, name) -> Parsed_EFpmax (expand_state_predicate g_decls pred1, name)
+  | Unexpanded_Parsed_EFtmin pred1 -> Parsed_EFtmin (expand_state_predicate g_decls pred1)
+  | Unexpanded_Parsed_Cycle_Through pred1 -> Parsed_Cycle_Through (expand_state_predicate g_decls pred1)
+  | Unexpanded_Parsed_Cycle_Through_generalized pred_list -> Parsed_Cycle_Through_generalized (List.map (expand_state_predicate g_decls) pred_list)
+  | Unexpanded_Parsed_NZ_Cycle -> Parsed_NZ_Cycle
+  | Unexpanded_Parsed_Deadlock_Freeness -> Parsed_Deadlock_Freeness
+  | Unexpanded_Parsed_IM pval -> Parsed_IM pval
+  | Unexpanded_Parsed_ConvexIM pval -> Parsed_ConvexIM pval
+  | Unexpanded_Parsed_PRP (pred1, pval) -> Parsed_PRP (expand_state_predicate g_decls pred1, pval)
+  | Unexpanded_Parsed_IMK pval -> Parsed_IMK pval
+  | Unexpanded_Parsed_IMunion pval -> Parsed_IMunion pval
+  | Unexpanded_Parsed_Cover_cartography (pdomain, n) -> Parsed_Cover_cartography (pdomain, n)
+  | Unexpanded_Parsed_Learning_cartography (pred1, pdomain, n) -> Parsed_Learning_cartography (expand_state_predicate g_decls pred1, pdomain, n)
+  | Unexpanded_Parsed_Shuffle_cartography (pdomain, n) -> Parsed_Shuffle_cartography (pdomain, n)
+  | Unexpanded_Parsed_Border_cartography (pdomain, n) -> Parsed_Border_cartography (pdomain, n)
+  | Unexpanded_Parsed_Random_cartography (pdomain, i, n) -> Parsed_Random_cartography (pdomain, i, n)
+  | Unexpanded_Parsed_RandomSeq_cartography (pdomain, i, n) -> Parsed_RandomSeq_cartography (pdomain, i, n)
+  | Unexpanded_Parsed_PRPC (pred1, pdomain, n) -> Parsed_PRPC (expand_state_predicate g_decls pred1, pdomain, n)
+  | Unexpanded_Parsed_pattern pattern -> Parsed_pattern pattern
+  | Unexpanded_Parsed_Win pred1 -> Parsed_Win (expand_state_predicate g_decls pred1)
+
+let expand_property (g_decls: variable_declarations) (property: unexpanded_parsed_property): parsed_property =
+  { synthesis_type = property.unexpanded_synthesis_type
+  ; property = expand_property_type g_decls property.unexpanded_property
+  ; projection = property.unexpanded_projection
+  }
diff --git a/src/lib/Templates.mli b/src/lib/Templates.mli
index d12dac6e..0810839b 100644
--- a/src/lib/Templates.mli
+++ b/src/lib/Templates.mli
@@ -1,3 +1,4 @@
 open ParsingStructure
 
 val expand_model : unexpanded_parsed_model -> parsed_model
+val expand_property : variable_declarations -> unexpanded_parsed_property -> parsed_property
diff --git a/tests/testcases/templates/properties/fischer.imi b/tests/testcases/templates/properties/fischer.imi
new file mode 100644
index 00000000..54fb0c0a
--- /dev/null
+++ b/tests/testcases/templates/properties/fischer.imi
@@ -0,0 +1,41 @@
+var
+    id : int;
+    k = 2 : constant;
+    IDLE = -1 : int;
+    N = 2 : int;
+
+synt_var
+    x : clock array (N);
+
+template p(i : int)
+
+loc A: invariant True
+  when id = IDLE do { x[i] := 0 } goto req;
+
+loc req: invariant x[i] <= k
+  when x[i] <= k do { x[i] := 0; id := i } goto waiting;
+
+loc waiting: invariant True
+  when id = IDLE do { x[i] := 0 } goto req;
+  when id = i & x[i] > k goto cs;
+
+loc cs: invariant True
+  when True do { id := IDLE } goto A;
+
+end
+
+forall i in [0, N - 1]: instantiate p[i] := p(i);
+
+init := {
+
+    discrete =
+        forall i in [0, N - 1]: loc[p[i]] := A,
+        id := IDLE,
+    ;
+
+    continuous =
+        forall i in [0, N - 1]: x[i] = i &
+    ;
+}
+
+end
diff --git a/tests/testcases/templates/properties/fischer.imiprop b/tests/testcases/templates/properties/fischer.imiprop
new file mode 100644
index 00000000..14745573
--- /dev/null
+++ b/tests/testcases/templates/properties/fischer.imiprop
@@ -0,0 +1,8 @@
+(* Does not work (needs parenthesis enclosing inner forall) *)
+(* property := #synth AGnot(forall i in [0, N - 1]: forall j in [0, N - 1]: loc[p[i]] <> cs) *)
+
+(* Works *)
+(* property := #synth AGnot(forall i in [0, N - 1]: (forall j in [0, N - 1]: loc[p[i]] <> cs)) *)
+
+(* Works -> True || False is outside of forall *)
+property := #synth AGnot(forall i in [0, N - 1]: loc[p[i]] <> cs && True || False)