Ltac:用回溯重复一个策略n次

假设我有一个类似的策略(摘自HaysTac),它寻找一个论点来专门化一个特定的假设:

Ltac find_specialize_in H :=
  multimatch goal with
  | [ v : _ |- _ ] => specialize (H v)
end.

不过,我想写一个策略 n 专门化战术的论据。关键是它需要回溯。例如,如果我有以下假设:

y : T
H : forall (x : T), x = y -> P x
x1 : T
x2 : T
Heq : x1 = y

do 2 (find_specialize_in H) x2