exact xs_ih ys_tl h1_right
binders : List (VarName × VarName)
xs_hd : VarName
xs_tl : List VarName
xs_ih : ∀ (ys : List VarName), isAlphaEqvVarList binders xs_tl ys → xs_tl.length = ys.length
ys_hd : VarName
ys_tl : List VarName
h1_left : isAlphaEqvVar binders xs_hd ys_hd
h1_right : isAlphaEqvVarList binders xs_tl ys_tl
⊢ xs_tl.length = ys_tl.length
no goals