induction F generalizing V j
D : Type
I : Interpretation D
V : VarAssignment D
z : String
F : Formula
j : ℕ
h1 : ¬occursIn (free_ z) F
h2 : Formula.lc_at j F
⊢ Holds D I V F ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] F)
case pred_
D : Type
I : Interpretation D
z a✝¹ : String
a✝ : List Var
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) (pred_ a✝¹ a✝)
h2 : Formula.lc_at j (pred_ a✝¹ a✝)
⊢ Holds D I V (pred_ a✝¹ a✝) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (pred_ a✝¹ a✝))

case not_
D : Type
I : Interpretation D
z : String
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) a✝ →
      Formula.lc_at j a✝ → (Holds D I V a✝ ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] a✝))
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) a✝.not_
h2 : Formula.lc_at j a✝.not_
⊢ Holds D I V a✝.not_ ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] a✝.not_)

case imp_
D : Type
I : Interpretation D
z : String
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) a✝¹ →
      Formula.lc_at j a✝¹ → (Holds D I V a✝¹ ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] a✝¹))
a_ih✝ :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) a✝ →
      Formula.lc_at j a✝ → (Holds D I V a✝ ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] a✝))
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) (a✝¹.imp_ a✝)
h2 : Formula.lc_at j (a✝¹.imp_ a✝)
⊢ Holds D I V (a✝¹.imp_ a✝) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (a✝¹.imp_ a✝))

case forall_
D : Type
I : Interpretation D
z a✝¹ : String
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D) (j : ℕ),
    ¬occursIn (free_ z) a✝ →
      Formula.lc_at j a✝ → (Holds D I V a✝ ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] a✝))
V : VarAssignment D
j : ℕ
h1 : ¬occursIn (free_ z) (forall_ a✝¹ a✝)
h2 : Formula.lc_at j (forall_ a✝¹ a✝)
⊢ Holds D I V (forall_ a✝¹ a✝) ↔ Holds D I (V ∘ Var.close j (free_ z)) (Formula.openList j [free_ z] (forall_ a✝¹ a✝))