case forall_ x phi phi_ih =>
  simp only [occursIn] at h1
  simp only [Formula.lc_at] at h2
  simp only [Formula.openList]
  simp only [Holds]
  apply forall_congr'
  intro d
  specialize phi_ih (shift D V d) (j + 1) h1 h2
  simp only [phi_ih]
  congr! 1
  apply extracted_1
D : Type
I : Interpretation D
z x : String
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) phi →
      Formula.lc_at j phi → (Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi))
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) (forall_ x phi)
h2 : Formula.lc_at j (forall_ x phi)
⊢ Holds D I V (forall_ x phi) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (forall_ x phi))
no goals