Automatically specializing hypotheses in Coq

Question

In proofs, if I perform induction on an argument that is not final, I get universally-quanitified induction hypotheses. I find myself repeatedly writing tactics like this:

match goal with
        | [H : forall (esub : expr) (x : exprvar) (tsub t : T) (Gamma_ : Gamma),
             (internalType Gamma_ ?Theta_ ?d esub tsub) ->
                        (internalType (gamma_evar x tsub :: ?Gamma_) ?Theta_ ?d ?e t)->
                        internalType Gamma_ ?Theta_ ?d (esubst_expr esub x ?e) t,
             esub : expr,
             xvar : exprvar,
             tsub : T,
             t : T,
             Gamma_ : Gamma,
             H1 : internalType ?Gamma_ ?Theta ?d ?esub ?xsub,
             H2 : internalType (gamma_evar ?xvar ?tsub :: ?Gamma_) ?Theta ?d ?e ?t
             |- _]

That is, I search for an inductive hypothesis, and for arguments that unify with it to specialize it. I then do specialize (Hypothesis Arg1 Arg2...)

This feels like boilerplate, but I keep having to write a different version for each lemma I use this on. Is there a way to:

1. do this automatically?
2. do this automatically, only for the induction hypotheses? (so that we don't get caught in infinite loops of applying every argument to every function possible)