by_cases c2 : v ∈ binders
case neg
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
h1_right_left : ∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1
h1_right_right : xs.length = (τ X xs.length).1.length
s1 :
  Holds D I (Function.updateListITE V (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2)
v : VarName
a1 : isFreeIn v (τ X xs.length).2
c1 : v ∉ (τ X xs.length).1
⊢ Function.updateListITE V (τ X xs.length).1 (List.map V xs) v =
    Function.updateListITE V' (τ X xs.length).1 (List.map V xs) v
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
h1_right_left : ∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1
h1_right_right : xs.length = (τ X xs.length).1.length
s1 :
  Holds D I (Function.updateListITE V (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2)
v : VarName
a1 : isFreeIn v (τ X xs.length).2
c1 : v ∉ (τ X xs.length).1
c2 : v ∈ binders
⊢ Function.updateListITE V (τ X xs.length).1 (List.map V xs) v =
    Function.updateListITE V' (τ X xs.length).1 (List.map V xs) v

case neg
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
h1_right_left : ∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1
h1_right_right : xs.length = (τ X xs.length).1.length
s1 :
  Holds D I (Function.updateListITE V (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2)
v : VarName
a1 : isFreeIn v (τ X xs.length).2
c1 : v ∉ (τ X xs.length).1
c2 : v ∉ binders
⊢ Function.updateListITE V (τ X xs.length).1 (List.map V xs) v =
    Function.updateListITE V' (τ X xs.length).1 (List.map V xs) v