How to access a parameter of a procedure in Pre/Post contracts of a procedure/funtion that has the the procedure as access parameter?

The Containers.Vector package defines some procedures that have an access to a procedure as parameter. This procedure supports one parameter.

Examples:

procedure Update_Element
  (Container : in out Vector;
   Index     : in     Index_Type;
   Process   : not null access procedure (E : in out Element_Type));

procedure Query_Element
  (Container : in Vector;
   Index     : in Index_Type;
   Process   : not null access procedure (E : in Element_Type));

Is it somehow possible to use E in the Pre and Post contracts of the procedures Query_Element and Update_Element?

Writing something like:

procedure Update_Element
  (Container : in out Vector;
   Index     : in     Index_Type;
   Process   : not null access procedure (E : in out Element_Type))
with Post => Element(Container,Index) = E;

Results in compilation error: "E" is undefined

If possible, the solution should be compatible with Spark.