intro v a1
case a.h.e'_1.a
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v psi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) psi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → V v = V' v
⊢ ∀ (v : VarName), isFreeIn v phi → V v = V' v
case a.h.e'_1.a
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V V' : VarAssignment D) (F : Formula),
    (∀ (v : VarName), isFreeIn v F → V v = V' v) → (Holds D I V tail✝ F ↔ Holds D I V' tail✝ F)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v phi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi)
psi_ih :
  ∀ (V V' : VarAssignment D),
    (∀ (v : VarName), isFreeIn v psi → V v = V' v) →
      (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) psi)
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v phi ∨ isFreeIn v psi → V v = V' v
v : VarName
a1 : isFreeIn v phi
⊢ V v = V' v