simp only [Holds] at h1
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V M E_tl (def_ name args) → ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
h1 : Holds D I V M (E_hd :: E_tl) (def_ name args)
⊢ ∃ d ∈ E_hd :: E_tl, name = d.name ∧ args.length = d.args.length
D : Type
I : Interpretation D
V : Valuation D
M : MetaValuation D
name : DefName
args : List VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V M E_tl (def_ name args) → ∃ d ∈ E_tl, name = d.name ∧ args.length = d.args.length
h1 :
  if name = E_hd.name ∧ args.length = E_hd.args.length then
    Holds D I (Function.updateListITE V E_hd.args (List.map V args)) M E_tl E_hd.F
  else Holds D I V M E_tl (def_ name args)
⊢ ∃ d ∈ E_hd :: E_tl, name = d.name ∧ args.length = d.args.length