Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
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')
phi psi : 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')
psi_ih :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders psi F' → (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
phi' psi' : Formula
h2_left : isAlphaEqvAux binders phi phi'
h2_right : isAlphaEqvAux binders psi psi'
⊢ (Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V (head✝ :: tail✝) psi) ↔
    (Holds D I V' (head✝ :: tail✝) phi' ↔ Holds D I V' (head✝ :: tail✝) psi')
Tactic:
congr! 1
Proof state after:
case a.h.e'_1.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')
phi psi : 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')
psi_ih :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders psi F' → (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
phi' psi' : Formula
h2_left : isAlphaEqvAux binders phi phi'
h2_right : isAlphaEqvAux binders psi psi'
⊢ Holds D I V (head✝ :: tail✝) phi ↔ Holds D I V' (head✝ :: tail✝) phi'

case a.h.e'_2.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')
phi psi : 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')
psi_ih :
  ∀ (V V' : VarAssignment D) (F' : Formula) (binders : List (VarName × VarName)),
    AlphaEqvVarAssignment D binders V V' →
      isAlphaEqvAux binders psi F' → (Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) F')
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
phi' psi' : Formula
h2_left : isAlphaEqvAux binders phi phi'
h2_right : isAlphaEqvAux binders psi psi'
⊢ Holds D I V (head✝ :: tail✝) psi ↔ Holds D I V' (head✝ :: tail✝) psi'