split_ifs
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
⊢ (if X = E_hd.name ∧ xs.length = E_hd.args.length then
      Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q
    else Holds D I V E_tl (def_ X (List.map σ xs))) ↔
    if X = E_hd.name ∧ xs.length = E_hd.args.length then
      Holds D I (Function.updateListITE (V ∘ σ) E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q
    else Holds D I (V ∘ σ) E_tl (def_ X xs)
case pos
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
h✝ : X = E_hd.name ∧ xs.length = E_hd.args.length
⊢ Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q ↔
    Holds D I (Function.updateListITE (V ∘ σ) E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q

case neg
D : Type
I : Interpretation D
c : Char
X : DefName
xs : List VarName
V : VarAssignment D
σ : VarName → VarName
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)
h✝ : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
⊢ Holds D I V E_tl (def_ X (List.map σ xs)) ↔ Holds D I (V ∘ σ) E_tl (def_ X xs)