Is there a tactic similar to “generalize dependent” in Coq?

Stream: lean4

[David Deng]

I am trying to prove the substitution lemma in logical relation, where the induction hypothesis (Γ ⊢ t : T) is independent of some variable γ:

lemma substitution : (Γ ⊢ t : T) → (γ ⊨ Γ) → (·⊨ (γ t) : T) :=

In Coq, I would do generalize dependent γ before doing induction on the typing derivation. I can get around it by redefining the lemma as:

lemma substitution : (Γ ⊢ t : T) → ∀ γ, (γ ⊨ Γ) → (·⊨ (γ t) : T) :=

and only introduce up to the typing derivation, which leaves γ universally quantified, thus being independent of the induction hypothesis.

But I wonder if there is anything similar to Coq where we can regain the independence?

[Aaron Liu]

Is induction ... generalizing γ what you are looking for?

[David Deng]

Yes. That's exactly what I am looking for. Thank you so much!

[David Deng]

Aaron Liu said:

Is induction ... generalizing γ what you are looking for?

Is there a list of tactics of all forms that I can use as a reference? For example, here is a coq to lean mapping, but I think it is for lean 3 rather than lean 4...

[Aaron Liu]

I know of this page.