[Hol-info] Instantiating existentials under existentials

[Magnus M. <mo...@ca...>]

Hi hol-info,

Quick question: is there a tactic for instantiating a nested
existential based on a name? Example: for a goal such as

  ?x y z. ... y ...

I want to use a tactic foo_tac `y` `5` and get:

  ?x z. ... 5 ...

Is there such a foo_tac tactic? I suspect this functionality is there
somewhere already. If not, then I'll implement it.

Note: I don't need the advanced feature of being able to instantiate
it with `x+z+1` where the variables refer to the other existentially
quantified variables.

Many thanks,
Magnus