cases h2
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : DefName
ys : List VarName
h2 : X = Y ∧ isAlphaEqvVarList binders xs ys
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : ¬(Y = hd.name ∧ ys.length = hd.args.length)
⊢ Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔ Holds D I V' tl (def_ Y ys)
case intro
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
ih :
  ∀ (V V' : VarAssignment D) (F F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' → isAlphaEqvAux binders F F' → (Holds D I V tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : DefName
ys : List VarName
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : ¬(Y = hd.name ∧ ys.length = hd.args.length)
left✝ : X = Y
right✝ : isAlphaEqvVarList binders xs ys
⊢ Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔ Holds D I V' tl (def_ Y ys)