induction F generalizing V j
D : Type
I : Interpretation D
V : VarAssignment D
j : ℕ
zs : List String
F : Formula
⊢ Holds D I (V ∘ Var.openList j (List.map free_ zs)) F ↔ Holds D I V (Formula.openList j (List.map free_ zs) F)
case pred_
D : Type
I : Interpretation D
zs : List String
a✝¹ : String
a✝ : List Var
V : VarAssignment D
j : ℕ
⊢ Holds D I (V ∘ Var.openList j (List.map free_ zs)) (pred_ a✝¹ a✝) ↔
    Holds D I V (Formula.openList j (List.map free_ zs) (pred_ a✝¹ a✝))

case not_
D : Type
I : Interpretation D
zs : List String
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) a✝ ↔ Holds D I V (Formula.openList j (List.map free_ zs) a✝)
V : VarAssignment D
j : ℕ
⊢ Holds D I (V ∘ Var.openList j (List.map free_ zs)) a✝.not_ ↔
    Holds D I V (Formula.openList j (List.map free_ zs) a✝.not_)

case imp_
D : Type
I : Interpretation D
zs : List String
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) a✝¹ ↔ Holds D I V (Formula.openList j (List.map free_ zs) a✝¹)
a_ih✝ :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) a✝ ↔ Holds D I V (Formula.openList j (List.map free_ zs) a✝)
V : VarAssignment D
j : ℕ
⊢ Holds D I (V ∘ Var.openList j (List.map free_ zs)) (a✝¹.imp_ a✝) ↔
    Holds D I V (Formula.openList j (List.map free_ zs) (a✝¹.imp_ a✝))

case forall_
D : Type
I : Interpretation D
zs : List String
a✝¹ : String
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D) (j : ℕ),
    Holds D I (V ∘ Var.openList j (List.map free_ zs)) a✝ ↔ Holds D I V (Formula.openList j (List.map free_ zs) a✝)
V : VarAssignment D
j : ℕ
⊢ Holds D I (V ∘ Var.openList j (List.map free_ zs)) (forall_ a✝¹ a✝) ↔
    Holds D I V (Formula.openList j (List.map free_ zs) (forall_ a✝¹ a✝))