diff --git a/meta_annotate.ml b/meta_annotate.ml
index c3a16fb6dd8273ce0aba5e802bdd62998b0df28c..a20ef3b96d7d1d369f01248e336885b3e34f02b1 100644
--- a/meta_annotate.ml
+++ b/meta_annotate.ml
@@ -242,7 +242,7 @@ class calling_visitor flags all_mp table = object (self)
 
   method calling_instance stmt called =
     let addr_term = addr_of_tlval called in
-    let assoc_list = [("\\called", addr_term)] in
+    let assoc_list = [("\\called", RepVariable addr_term)] in
     List.iter (self # instantiate stmt assoc_list) mp_todo
 
   method! vinst = function
@@ -317,7 +317,7 @@ class writing_visitor flags all_mp table = object(self)
     | TVar lv, _ when flags.simpl && Meta_simplify.is_not_orig_variable lv -> ()
     | written ->
       let addr_term = addr_of_tlval written in
-      let assoc_list = [("\\written", addr_term)] in
+      let assoc_list = [("\\written", RepVariable addr_term)] in
       List.iter (self # instantiate ~post stmt assoc_list) mp_todo
 
   (* Inspect function specs to see what it assigns and instantiate the
@@ -384,7 +384,7 @@ class reading_visitor flags all_mp table = object (self)
   (* Instantiates the property while replacing \read terms *)
   method reading_instance ?post stmt written =
     let addr_term = addr_of_tlval written in
-    let assoc_list = [("\\read", addr_term)] in
+    let assoc_list = [("\\read", RepVariable addr_term)] in
     List.iter (self#instantiate ~post stmt assoc_list) mp_todo
 
   (* Hashtable : stmt -> set of tlvals used in it. Used to avoid duplicate
diff --git a/meta_deduce.ml b/meta_deduce.ml
index 23a946c27b98d36fd702db6f6346130b7d7d3cc8..58dca2d6ac7a8967fb3d91249159484539d10d85 100644
--- a/meta_deduce.ml
+++ b/meta_deduce.ml
@@ -118,7 +118,7 @@ let dummy_term loc = {
 
 let dummy_unpack mp =
   let terms = ["\\written"; "\\read"; "\\called"] in
-  let assoc = List.map (fun t -> (t, dummy_term mp.mp_loc)) terms in
+  let assoc = List.map (fun t -> (t, RepVariable (dummy_term mp.mp_loc))) terms in
   mp.mp_property (Kernel_function.dummy ()) assoc
 
 let predicate_counter = ref 1
diff --git a/meta_dispatch.ml b/meta_dispatch.ml
index 2a05910192aa11976581a83ee07d72fb78796dc4..923996fd841c03219d75db88d4864b0c0adf77b7 100644
--- a/meta_dispatch.ml
+++ b/meta_dispatch.ml
@@ -26,7 +26,7 @@ open Meta_options
 
 type unpacked_metaproperty = {
   ump_emitter : Emitter.t;
-  ump_property : Kernel_function.t -> ?stmt:stmt -> (string * term) list -> predicate;
+  ump_property : Kernel_function.t -> ?stmt:stmt -> (string * replaced_kind) list -> predicate;
   ump_ip : Property.t;
   ump_counter : int ref;
   ump_admit : bool;
diff --git a/meta_dispatch.mli b/meta_dispatch.mli
index 3232d36291d53e0260d8e77ba37d14b2dbc115c7..dd72b00c6ffe9427ea869085704dc19c713eff80 100644
--- a/meta_dispatch.mli
+++ b/meta_dispatch.mli
@@ -26,7 +26,7 @@ open Meta_options
 
 type unpacked_metaproperty = {
   ump_emitter : Emitter.t;
-  ump_property : Kernel_function.t -> ?stmt:stmt -> (string * term) list -> predicate;
+  ump_property : Kernel_function.t -> ?stmt:stmt -> (string * replaced_kind) list -> predicate;
   ump_ip : Property.t;
   ump_counter : int ref;
   ump_admit : bool;
diff --git a/meta_parse.ml b/meta_parse.ml
index a76054e177811335979677b4f45241c09373fbd5..252d8b4d9ccd254620c73582d6eeac204272916e 100644
--- a/meta_parse.ml
+++ b/meta_parse.ml
@@ -59,11 +59,16 @@ type mp_translation =
   | MtDefault (* translation activated, with unspecified mode *)
   | MtNone
 
+(* Kinds of keywords that can be replaced in a MP instantiation *)
+type replaced_kind =
+  | RepVariable of term (* replace variable by term *)
+  | RepApp of (string * term) list (* replace application with arg by associated term *)
+
 type metaproperty = {
   mp_name : string;
   mp_target : target;
   mp_context : context;
-  mp_property : Kernel_function.t -> (string * term) list -> predicate;
+  mp_property : Kernel_function.t -> (string * replaced_kind) list -> predicate;
   mp_proof_method : mp_proof_method;
   mp_translation : mp_translation;
   mp_loc : Cil_types.location
@@ -142,7 +147,11 @@ let meta_type_term termassoc quantifiers kf loc orig_ctxt meta_ctxt env expr =
     | PLapp ("\\bound", _, [bound]) ->
       Meta_bindings.parse_bound meta_ctxt loc quantifiers bound
     | PLvar vname when List.mem vname mp_terms ->
-      begin try List.assoc vname termassoc
+      begin try
+        begin match List.assoc vname termassoc with
+          | RepVariable a -> a
+          | _ -> assert false
+        end
       with _ -> meta_ctxt.error loc
                   "Variable %s forbidden in this context" vname
       end
@@ -197,8 +206,15 @@ let rec process_targets tc expr = match expr.lexpr_node with
   | _ -> TgSet (StrSet.singleton @@ process_single_target tc expr)
 
 let pp_aslist fmt l =
+  let pp_replaced_kind fmt = function
+    | RepVariable v -> Printer.pp_term fmt v
+    | RepApp l ->
+      let pp_singular fmt (a, b) =
+        Format.fprintf fmt "(%s, %a)" a Printer.pp_term b
+      in Format.pp_print_list pp_singular fmt l
+  in
   let pp_assoc fmt (a, b) =
-    Format.fprintf fmt "(%s, %a)" a Printer.pp_term b
+    Format.fprintf fmt "(%s, %a)" a pp_replaced_kind b
   in Format.pp_print_list pp_assoc fmt l
 
 let delay_prop tc name lexpr kf aslist =
diff --git a/meta_parse.mli b/meta_parse.mli
index 712af9408160c401eb83dfeb9c8deec874ab6241..a2efca88d3ac5e3a663f292e5c1f2279b7002c9d 100644
--- a/meta_parse.mli
+++ b/meta_parse.mli
@@ -53,11 +53,15 @@ type mp_translation =
   | MtDefault
   | MtNone
 
+type replaced_kind =
+  | RepVariable of term (* replace variable by term *)
+  | RepApp of (string * term) list (* replace application with arg by associated term *)
+
 type metaproperty = {
   mp_name : string;
   mp_target : target;
   mp_context : context;
-  mp_property : Kernel_function.t -> (string * term) list -> predicate;
+  mp_property : Kernel_function.t -> (string * replaced_kind) list -> predicate;
   mp_proof_method : mp_proof_method;
   mp_translation : mp_translation;
   mp_loc : Cil_types.location