induction E
D : Type
I : Interpretation D
E : Env
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) E (def_ h1_X h1_xs) ↔
    Holds D I V E (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
case nil
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) [] (def_ h1_X h1_xs) ↔
    Holds D I V [] (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))

case cons
D : Type
I : Interpretation D
v t : VarName
F F' : Formula
h1_X : DefName
h1_xs : List VarName
h1_v h1_t : VarName
V : VarAssignment D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  Holds D I (Function.updateITE V h1_v (V h1_t)) tail✝ (def_ h1_X h1_xs) ↔
    Holds D I V tail✝ (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))
⊢ Holds D I (Function.updateITE V h1_v (V h1_t)) (head✝ :: tail✝) (def_ h1_X h1_xs) ↔
    Holds D I V (head✝ :: tail✝) (def_ h1_X (List.map (fun x => if h1_v = x then h1_t else x) h1_xs))