simp only [Sub.Var.One.Rec.fastReplaceFree]
D : Type
I : Interpretation D
u v : VarName
a : D
X : DefName
xs : List VarName
V : VarAssignment D
h1 : ¬isFreeIn v (def_ X xs)
h2 : ¬isBoundIn v (def_ X xs)
⊢ Holds D I (Function.updateITE V u a) [] (def_ X xs) ↔
    Holds D I (Function.updateITE V v a) [] (Sub.Var.One.Rec.fastReplaceFree u v (def_ X xs))
D : Type
I : Interpretation D
u v : VarName
a : D
X : DefName
xs : List VarName
V : VarAssignment D
h1 : ¬isFreeIn v (def_ X xs)
h2 : ¬isBoundIn v (def_ X xs)
⊢ Holds D I (Function.updateITE V u a) [] (def_ X xs) ↔
    Holds D I (Function.updateITE V v a) [] (def_ X (List.map (fun x => if u = x then v else x) xs))