case pred_ X vs =>
  simp only [occursIn] at h1
  simp only [Formula.lc_at] at h2
  simp only [Formula.openList]
  simp only [Holds]
  congr! 1
  simp
  simp only [List.map_eq_map_iff]
  intro v a1
  specialize h2 v a1
  simp
  cases v
  case _ x =>
    simp only [Var.openList]
    simp only [Var.close]
    have s1 : ¬ free_ x = free_ z
    intro contra
    apply h1
    simp only [← contra]
    exact a1
    simp only [if_neg s1]
  case _ i =>
    simp only [Var.lc_at] at h2
    simp only [Var.openList]
    simp
    split_ifs
    simp only [Var.close]
    simp only [if_pos h2]
D : Type
I : Interpretation D
z X : String
vs : List Var
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) (pred_ X vs)
h2 : Formula.lc_at j (pred_ X vs)
⊢ Holds D I V (pred_ X vs) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (pred_ X vs))
no goals