simp only [eq_comm]
case h1.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
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : Y = hd.name ∧ ys.length = hd.args.length
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
v : VarName
a1 : isFreeIn v hd.q
⊢ hd.args.length = ys.length
case h1.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
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : Y = hd.name ∧ ys.length = hd.args.length
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
v : VarName
a1 : isFreeIn v hd.q
⊢ ys.length = hd.args.length