push_neg at h1
D : Type
I : Interpretation D
z : String
phi psi : 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))
psi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) psi →
      Formula.lc_at j psi → (Holds D I V psi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] psi))
V : VarAssignment D
j : ℕ
h1 : ¬(occursIn (free_ z) phi ∨ occursIn (free_ z) psi)
h2 : Formula.lc_at j (phi.imp_ psi)
⊢ Holds D I V (phi.imp_ psi) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (phi.imp_ psi))
D : Type
I : Interpretation D
z : String
phi psi : 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))
psi_ih :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) psi →
      Formula.lc_at j psi → (Holds D I V psi ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] psi))
V : VarAssignment D
j : ℕ
h2 : Formula.lc_at j (phi.imp_ psi)
h1 : ¬occursIn (free_ z) phi ∧ ¬occursIn (free_ z) psi
⊢ Holds D I V (phi.imp_ psi) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (phi.imp_ psi))