case nil.def_.def_ =>
  simp only [Holds]
D : Type
I : Interpretation D
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 [] (def_ a✝³ a✝²) ↔ Holds D I V' [] (def_ a✝¹ a✝)
no goals