Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
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 tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : DefName
ys : List VarName
h2 : X = Y ∧ isAlphaEqvVarList binders xs ys
⊢ (if X = hd.name ∧ xs.length = hd.args.length then Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
    else Holds D I V tl (def_ X xs)) ↔
    if Y = hd.name ∧ ys.length = hd.args.length then
      Holds D I (Function.updateListITE V' hd.args (List.map V' ys)) tl hd.q
    else Holds D I V' tl (def_ Y ys)
Tactic:
split_ifs
Proof state after:
case pos
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
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 tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : DefName
ys : List VarName
h2 : X = Y ∧ isAlphaEqvVarList binders xs ys
h✝¹ : X = hd.name ∧ xs.length = hd.args.length
h✝ : Y = hd.name ∧ ys.length = hd.args.length
⊢ Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔
    Holds D I (Function.updateListITE V' hd.args (List.map V' ys)) tl hd.q

case neg
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
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 tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : DefName
ys : List VarName
h2 : X = Y ∧ isAlphaEqvVarList binders xs ys
h✝¹ : X = hd.name ∧ xs.length = hd.args.length
h✝ : ¬(Y = hd.name ∧ ys.length = hd.args.length)
⊢ Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔ Holds D I V' tl (def_ Y ys)

case pos
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
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 tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : DefName
ys : List VarName
h2 : X = Y ∧ isAlphaEqvVarList binders xs ys
h✝¹ : ¬(X = hd.name ∧ xs.length = hd.args.length)
h✝ : Y = hd.name ∧ ys.length = hd.args.length
⊢ Holds D I V tl (def_ X xs) ↔ Holds D I (Function.updateListITE V' hd.args (List.map V' ys)) tl hd.q

case neg
D : Type
I : Interpretation D
hd : Definition
tl : List Definition
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 tl F ↔ Holds D I V' tl F')
X : DefName
xs : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
Y : DefName
ys : List VarName
h2 : X = Y ∧ isAlphaEqvVarList binders xs ys
h✝¹ : ¬(X = hd.name ∧ xs.length = hd.args.length)
h✝ : ¬(Y = hd.name ∧ ys.length = hd.args.length)
⊢ Holds D I V tl (def_ X xs) ↔ Holds D I V' tl (def_ Y ys)