simp only [Holds]
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✝)
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
⊢ (if a✝¹ = head✝.name ∧ a✝.length = head✝.args.length then
      Holds D I (Function.updateListITE V head✝.args (List.map V a✝)) tail✝ head✝.q
    else Holds D I V tail✝ (def_ a✝¹ a✝)) ↔
    if a✝¹ = head✝.name ∧ a✝.length = head✝.args.length then
      Holds D I (Function.updateListITE V' head✝.args (List.map V' a✝)) tail✝ head✝.q
    else Holds D I V' tail✝ (def_ a✝¹ a✝)