Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
case h1
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
h1_binders : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
h1_1 : AlphaEqvVarAssignment D h1_binders h1_V h1_V'
a_ih✝ :
  isAlphaEqvAux ((x, y) :: h1_binders) phi phi' →
    (Holds D I (Function.updateITE h1_V x d) (head✝ :: tail✝) phi ↔
      Holds D I (Function.updateITE h1_V' y d) (head✝ :: tail✝) phi')
h2 : isAlphaEqvAux ((x, y) :: (h1_x, h1_y) :: h1_binders) phi phi'
⊢ AlphaEqvVarAssignment D ?binders (Function.updateITE (Function.updateITE h1_V h1_x h1_d) x d)
    (Function.updateITE (Function.updateITE h1_V' h1_y h1_d) y d)
Tactic:
apply AlphaEqvVarAssignment.cons
Proof state after:
case h1.a
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
h1_binders : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
h1_1 : AlphaEqvVarAssignment D h1_binders h1_V h1_V'
a_ih✝ :
  isAlphaEqvAux ((x, y) :: h1_binders) phi phi' →
    (Holds D I (Function.updateITE h1_V x d) (head✝ :: tail✝) phi ↔
      Holds D I (Function.updateITE h1_V' y d) (head✝ :: tail✝) phi')
h2 : isAlphaEqvAux ((x, y) :: (h1_x, h1_y) :: h1_binders) phi phi'
⊢ AlphaEqvVarAssignment D ?h1.binders (Function.updateITE h1_V h1_x h1_d) (Function.updateITE h1_V' h1_y h1_d)

case h1.binders
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
h1_binders : List (VarName × VarName)
h1_x h1_y : VarName
h1_V h1_V' : VarAssignment D
h1_d : D
h1_1 : AlphaEqvVarAssignment D h1_binders h1_V h1_V'
a_ih✝ :
  isAlphaEqvAux ((x, y) :: h1_binders) phi phi' →
    (Holds D I (Function.updateITE h1_V x d) (head✝ :: tail✝) phi ↔
      Holds D I (Function.updateITE h1_V' y d) (head✝ :: tail✝) phi')
h2 : isAlphaEqvAux ((x, y) :: (h1_x, h1_y) :: h1_binders) phi phi'
⊢ List (VarName × VarName)