simp only [Holds]
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
⊢ Holds D I V (E1_hd :: (E1_tl ++ E)) (def_ X xs) ↔ Holds D I V E (def_ X xs)
D : Type
I : Interpretation D
E : Env
X : DefName
xs : List VarName
V : VarAssignment D
a E1_hd : Definition
E1_tl : List Definition
E1_ih :
  List.Pairwise (fun d1 d2 => d1.name = d2.name → d1.args.length = d2.args.length → False) (E1_tl ++ E) →
    (Holds D I V (E1_tl ++ E) (def_ X xs) ↔ Holds D I V E (def_ X xs))
h2_1_left : a ∈ E
h2_1_right_left : X = a.name
h2_1_right_right : xs.length = a.args.length
h3_left : ∀ (a' : Definition), a' ∈ E1_tl ∨ a' ∈ E → E1_hd.name = a'.name → ¬E1_hd.args.length = a'.args.length
h3_right : List.Pairwise (fun d1 d2 => d1.name = d2.name → ¬d1.args.length = d2.args.length) (E1_tl ++ E)
⊢ (if X = E1_hd.name ∧ xs.length = E1_hd.args.length then
      Holds D I (Function.updateListITE V E1_hd.args (List.map V xs)) (E1_tl ++ E) E1_hd.q
    else Holds D I V (E1_tl ++ E) (def_ X xs)) ↔
    Holds D I V E (def_ X xs)