simp only [isAlphaEqvAux] at h2
case cons.def_.def_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_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 tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : DefName
a✝² : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : DefName
a✝ : List VarName
h2 : isAlphaEqvAux binders (def_ a✝³ a✝²) (def_ a✝¹ a✝)
⊢ Holds D I V (head✝ :: tail✝) (def_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (def_ a✝¹ a✝)
case cons.def_.def_
D : Type
I : Interpretation D
head✝ : Definition
tail✝ : List Definition
tail_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 tail✝ F ↔ Holds D I V' tail✝ F')
a✝³ : DefName
a✝² : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : DefName
a✝ : List VarName
h2 : a✝³ = a✝¹ ∧ isAlphaEqvVarList binders a✝² a✝
⊢ Holds D I V (head✝ :: tail✝) (def_ a✝³ a✝²) ↔ Holds D I V' (head✝ :: tail✝) (def_ a✝¹ a✝)