induction F generalizing V V'
D : Type
I : Interpretation D
V V' : VarAssignment D
F : Formula
h1 : ∀ (v : Var), occursFreeIn v F → V v = V' v
⊢ Holds D I V F ↔ Holds D I V' F
case pred_
D : Type
I : Interpretation D
a✝¹ : String
a✝ : List Var
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn v (pred_ a✝¹ a✝) → V v = V' v
⊢ Holds D I V (pred_ a✝¹ a✝) ↔ Holds D I V' (pred_ a✝¹ a✝)

case not_
D : Type
I : Interpretation D
a✝ : Formula
a_ih✝ : ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v a✝ → V v = V' v) → (Holds D I V a✝ ↔ Holds D I V' a✝)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn v a✝.not_ → V v = V' v
⊢ Holds D I V a✝.not_ ↔ Holds D I V' a✝.not_

case imp_
D : Type
I : Interpretation D
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v a✝¹ → V v = V' v) → (Holds D I V a✝¹ ↔ Holds D I V' a✝¹)
a_ih✝ : ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v a✝ → V v = V' v) → (Holds D I V a✝ ↔ Holds D I V' a✝)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn v (a✝¹.imp_ a✝) → V v = V' v
⊢ Holds D I V (a✝¹.imp_ a✝) ↔ Holds D I V' (a✝¹.imp_ a✝)

case forall_
D : Type
I : Interpretation D
a✝¹ : String
a✝ : Formula
a_ih✝ : ∀ (V V' : VarAssignment D), (∀ (v : Var), occursFreeIn v a✝ → V v = V' v) → (Holds D I V a✝ ↔ Holds D I V' a✝)
V V' : VarAssignment D
h1 : ∀ (v : Var), occursFreeIn v (forall_ a✝¹ a✝) → V v = V' v
⊢ Holds D I V (forall_ a✝¹ a✝) ↔ Holds D I V' (forall_ a✝¹ a✝)