induction h1
case h
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')
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders phi F' → (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
y : VarName
phi' : Formula
h2 : isAlphaEqvAux ((x, y) :: binders) phi phi'
d : D
⊢ Holds D I (Function.updateITE V x d) (head✝ :: tail✝) phi ↔
    Holds D I (Function.updateITE V' y d) (head✝ :: tail✝) phi'
case h.nil
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')
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders phi F' → (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
y : VarName
phi' : Formula
d : D
V✝ : VarAssignment D
h2 : isAlphaEqvAux [(x, y)] phi phi'
⊢ Holds D I (Function.updateITE V✝ x d) (head✝ :: tail✝) phi ↔
    Holds D I (Function.updateITE V✝ y d) (head✝ :: tail✝) phi'

case h.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')
x : VarName
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders phi F' → (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
y : VarName
phi' : Formula
d : D
binders✝ : List (VarName × VarName)
x✝ y✝ : VarName
V✝ V'✝ : VarAssignment D
d✝ : D
a✝ : AlphaEqvVarAssignment D binders✝ V✝ V'✝
a_ih✝ :
  isAlphaEqvAux ((x, y) :: binders✝) phi phi' →
    (Holds D I (Function.updateITE V✝ x d) (head✝ :: tail✝) phi ↔
      Holds D I (Function.updateITE V'✝ y d) (head✝ :: tail✝) phi')
h2 : isAlphaEqvAux ((x, y) :: (x✝, y✝) :: binders✝) phi phi'
⊢ Holds D I (Function.updateITE (Function.updateITE V✝ x✝ d✝) x d) (head✝ :: tail✝) phi ↔
    Holds D I (Function.updateITE (Function.updateITE V'✝ y✝ d✝) y d) (head✝ :: tail✝) phi'