exact phi_ih V j h1 h2
case a.h.e'_1.a
D : Type
I : Interpretation D
z : 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 phi
⊢ Holds D I V phi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] phi)
no goals