induction E generalizing F F' binders V V'
D : Type
I : Interpretation D
V V' : VarAssignment D
E : Env
F F' : Formula
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
h2 : isAlphaEqvAux binders F F'
⊢ Holds D I V E F ↔ Holds D I V' E F'
case nil
D : Type
I : Interpretation D
V V' : VarAssignment D
F F' : Formula
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
h2 : isAlphaEqvAux binders F F'
⊢ Holds D I V [] F ↔ Holds D I V' [] F'

case cons
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')
V V' : VarAssignment D
F F' : Formula
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
h2 : isAlphaEqvAux binders F F'
⊢ Holds D I V (head✝ :: tail✝) F ↔ Holds D I V' (head✝ :: tail✝) F'