simp only [isFreeIn] at h1
case cons.def_
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)
a✝¹ : DefName
a✝ : List VarName
V V' : VarAssignment D
h1 : ∀ (v : VarName), isFreeIn v (def_ a✝¹ a✝) → V v = V' v
⊢ Holds D I V (head✝ :: tail✝) (def_ a✝¹ a✝) ↔ Holds D I V' (head✝ :: tail✝) (def_ a✝¹ a✝)
case cons.def_
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)
a✝¹ : DefName
a✝ : List VarName
V V' : VarAssignment D
h1 : ∀ v ∈ a✝, V v = V' v
⊢ Holds D I V (head✝ :: tail✝) (def_ a✝¹ a✝) ↔ Holds D I V' (head✝ :: tail✝) (def_ a✝¹ a✝)