specialize phi_ih (shift D V d) (j + 1) h1 h2
case h
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) phi
h2 : Formula.lc_at (j + 1) phi
d : D
⊢ Holds D I (shift D V d) phi ↔
    Holds D I (shift D (V ∘ Var.close j (free_ z)) d) (Formula.openList (j + 1) [free_ z] phi)
case h
D : Type
I : Interpretation D
z x : String
phi : Formula
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) phi
h2 : Formula.lc_at (j + 1) phi
d : D
phi_ih :
  Holds D I (shift D V d) phi ↔
    Holds D I (shift D V d ∘ Var.close (j + 1) (free_ z)) (Formula.openList (j + 1) [free_ z] phi)
⊢ Holds D I (shift D V d) phi ↔
    Holds D I (shift D (V ∘ Var.close j (free_ z)) d) (Formula.openList (j + 1) [free_ z] phi)