Theorem: FOL.NV.isAlphaEqv_Holds_aux (FOL/NV/Alpha.lean)

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_V : VarAssignment D
h2 : isAlphaEqvAux [(x, y)] phi phi'
⊢ AlphaEqvVarAssignment D ?binders (Function.updateITE h1_V x d) (Function.updateITE h1_V y d)
Tactic:
apply AlphaEqvVarAssignment.cons
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_V : VarAssignment D
h2 : isAlphaEqvAux [(x, y)] phi phi'
⊢ AlphaEqvVarAssignment D ?h1.binders h1_V h1_V

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_V : VarAssignment D
h2 : isAlphaEqvAux [(x, y)] phi phi'
⊢ List (VarName × VarName)

State before:
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_V : VarAssignment D
h2 : isAlphaEqvAux [(x, y)] phi phi'
⊢ AlphaEqvVarAssignment D ?h1.binders h1_V h1_V

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_V : VarAssignment D
h2 : isAlphaEqvAux [(x, y)] phi phi'
⊢ List (VarName × VarName)
Tactic:
apply AlphaEqvVarAssignment.nil
State after:
no goals

State before:
case h2
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_V : VarAssignment D
h2 : isAlphaEqvAux [(x, y)] phi phi'
⊢ isAlphaEqvAux [(x, y)] phi phi'
Tactic:
exact h2
State after:
no goals

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')
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'
⊢ Holds D I (Function.updateITE (Function.updateITE h1_V h1_x h1_d) x d) (head✝ :: tail✝) phi ↔
    Holds D I (Function.updateITE (Function.updateITE h1_V' h1_y h1_d) y d) (head✝ :: tail✝) phi'
Tactic:
apply phi_ih
State after:
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)

case h2
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'
⊢ isAlphaEqvAux ?binders phi phi'

case 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)

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
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)

State before:
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)
Tactic:
apply AlphaEqvVarAssignment.cons
State after:
case h1.a.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.a.binders h1_V h1_V'

case h1.a.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)

State before:
case h1.a.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.a.binders h1_V h1_V'

case h1.a.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)
Tactic:
exact h1_1
State after:
no goals

State before:
case h2
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'
⊢ isAlphaEqvAux ((x, y) :: (h1_x, h1_y) :: h1_binders) phi phi'
Tactic:
exact h2
State after:
no goals

State before:
D : Type
I : Interpretation D
a✝³ : DefName
a✝² : List VarName
V V' : VarAssignment D
binders : List (VarName × VarName)
h1 : AlphaEqvVarAssignment D binders V V'
a✝¹ : DefName
a✝ : List VarName
h2 : a✝³ = a✝¹ ∧ isAlphaEqvVarList binders a✝² a✝
⊢ Holds D I V [] (def_ a✝³ a✝²) ↔ Holds D I V' [] (def_ a✝¹ a✝)
Tactic:
simp only [Holds]
State after:
no goals

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
⊢ Holds D I V (hd :: tl) (def_ X xs) ↔ Holds D I V' (hd :: tl) (def_ Y ys)
Tactic:
simp only [Holds]
State after:
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)

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
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)

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
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : ¬(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)
Tactic:
case _ c1 c2 =>
  cases h2
  case intro h2_left h2_right =>
    simp only [isAlphaEqvVarList_length binders xs ys h2_right] at c1
    subst h2_left
    contradiction
State after:
no goals

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
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
c2 : 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
Tactic:
case _ c1 c2 =>
  cases h2
  case intro h2_left h2_right =>
    simp only [← isAlphaEqvVarList_length binders xs ys h2_right] at c2
    subst h2_left
    contradiction
State after:
no goals

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
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
c2 : ¬(Y = hd.name ∧ ys.length = hd.args.length)
⊢ Holds D I V tl (def_ X xs) ↔ Holds D I V' tl (def_ Y ys)
Tactic:
case _ c1 c2 =>
  exact ih V V' (def_ X xs) (def_ Y ys) binders h1 h2
State after:
no goals

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
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : 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
Tactic:
cases h2
State after:
case intro
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
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : Y = hd.name ∧ ys.length = hd.args.length
left✝ : X = Y
right✝ : isAlphaEqvVarList binders xs ys
⊢ 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

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
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : Y = hd.name ∧ ys.length = hd.args.length
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
⊢ 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
Tactic:
apply Holds_coincide_Var
State after:
case h1
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
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : Y = hd.name ∧ ys.length = hd.args.length
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
⊢ ∀ (v : VarName),
    isFreeIn v hd.q →
      Function.updateListITE V hd.args (List.map V xs) v = Function.updateListITE V' hd.args (List.map V' ys) v

State before:
case h1
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
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : Y = hd.name ∧ ys.length = hd.args.length
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
⊢ ∀ (v : VarName),
    isFreeIn v hd.q →
      Function.updateListITE V hd.args (List.map V xs) v = Function.updateListITE V' hd.args (List.map V' ys) v
Tactic:
intro v a1
State after:
case h1
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
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : Y = hd.name ∧ ys.length = hd.args.length
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
v : VarName
a1 : isFreeIn v hd.q
⊢ Function.updateListITE V hd.args (List.map V xs) v = Function.updateListITE V' hd.args (List.map V' ys) v

State before:
case h1
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
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : Y = hd.name ∧ ys.length = hd.args.length
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
v : VarName
a1 : isFreeIn v hd.q
⊢ Function.updateListITE V hd.args (List.map V xs) v = Function.updateListITE V' hd.args (List.map V' ys) v
Tactic:
simp only [aux_2 D binders xs ys V V' h1 h2_right]
State after:
case h1
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
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : Y = hd.name ∧ ys.length = hd.args.length
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
v : VarName
a1 : isFreeIn v hd.q
⊢ Function.updateListITE V hd.args (List.map V' ys) v = Function.updateListITE V' hd.args (List.map V' ys) v

State before:
case h1
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
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : Y = hd.name ∧ ys.length = hd.args.length
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
v : VarName
a1 : isFreeIn v hd.q
⊢ Function.updateListITE V hd.args (List.map V' ys) v = Function.updateListITE V' hd.args (List.map V' ys) v
Tactic:
apply Function.updateListITE_mem_eq_len
State after:
case h1.h1
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
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : Y = hd.name ∧ ys.length = hd.args.length
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
v : VarName
a1 : isFreeIn v hd.q
⊢ v ∈ hd.args

case h1.h2
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
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : Y = hd.name ∧ ys.length = hd.args.length
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
v : VarName
a1 : isFreeIn v hd.q
⊢ hd.args.length = (List.map V' ys).length

State before:
case h1.h1
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
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : Y = hd.name ∧ ys.length = hd.args.length
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
v : VarName
a1 : isFreeIn v hd.q
⊢ v ∈ hd.args
Tactic:
simp only [isFreeIn_iff_mem_freeVarSet] at a1
State after:
case h1.h1
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
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : Y = hd.name ∧ ys.length = hd.args.length
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
v : VarName
a1 : v ∈ hd.q.freeVarSet
⊢ v ∈ hd.args

State before:
case h1.h1
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
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : Y = hd.name ∧ ys.length = hd.args.length
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
v : VarName
a1 : v ∈ hd.q.freeVarSet
⊢ v ∈ hd.args
Tactic:
simp only [← List.mem_toFinset]
State after:
case h1.h1
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
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : Y = hd.name ∧ ys.length = hd.args.length
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
v : VarName
a1 : v ∈ hd.q.freeVarSet
⊢ v ∈ hd.args.toFinset

State before:
case h1.h1
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
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : Y = hd.name ∧ ys.length = hd.args.length
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
v : VarName
a1 : v ∈ hd.q.freeVarSet
⊢ v ∈ hd.args.toFinset
Tactic:
apply Finset.mem_of_subset hd.h1 a1
State after:
no goals

State before:
case h1.h2
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
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : Y = hd.name ∧ ys.length = hd.args.length
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
v : VarName
a1 : isFreeIn v hd.q
⊢ hd.args.length = (List.map V' ys).length
Tactic:
simp
State after:
case h1.h2
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
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : Y = hd.name ∧ ys.length = hd.args.length
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
v : VarName
a1 : isFreeIn v hd.q
⊢ hd.args.length = ys.length

State before:
case h1.h2
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
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : Y = hd.name ∧ ys.length = hd.args.length
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
v : VarName
a1 : isFreeIn v hd.q
⊢ hd.args.length = ys.length
Tactic:
simp only [eq_comm]
State after:
case h1.h2
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
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : Y = hd.name ∧ ys.length = hd.args.length
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
v : VarName
a1 : isFreeIn v hd.q
⊢ ys.length = hd.args.length

State before:
case h1.h2
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
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : Y = hd.name ∧ ys.length = hd.args.length
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
v : VarName
a1 : isFreeIn v hd.q
⊢ ys.length = hd.args.length
Tactic:
cases c2
State after:
case h1.h2.intro
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
c1 : X = hd.name ∧ xs.length = hd.args.length
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
v : VarName
a1 : isFreeIn v hd.q
left✝ : Y = hd.name
right✝ : ys.length = hd.args.length
⊢ ys.length = hd.args.length

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
c1 : X = hd.name ∧ xs.length = hd.args.length
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
v : VarName
a1 : isFreeIn v hd.q
c2_left : Y = hd.name
c2_right : ys.length = hd.args.length
⊢ ys.length = hd.args.length
Tactic:
case intro c2_left c2_right =>
  exact c2_right
State after:
no goals

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
c1 : X = hd.name ∧ xs.length = hd.args.length
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
v : VarName
a1 : isFreeIn v hd.q
c2_left : Y = hd.name
c2_right : ys.length = hd.args.length
⊢ ys.length = hd.args.length
Tactic:
exact c2_right
State after:
no goals

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
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : ¬(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)
Tactic:
cases h2
State after:
case intro
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
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : ¬(Y = hd.name ∧ ys.length = hd.args.length)
left✝ : X = Y
right✝ : isAlphaEqvVarList binders xs ys
⊢ Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔ Holds D I V' tl (def_ Y ys)

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
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : ¬(Y = hd.name ∧ ys.length = hd.args.length)
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
⊢ Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔ Holds D I V' tl (def_ Y ys)
Tactic:
case intro h2_left h2_right =>
  simp only [isAlphaEqvVarList_length binders xs ys h2_right] at c1
  subst h2_left
  contradiction
State after:
no goals

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
c1 : X = hd.name ∧ xs.length = hd.args.length
c2 : ¬(Y = hd.name ∧ ys.length = hd.args.length)
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
⊢ Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔ Holds D I V' tl (def_ Y ys)
Tactic:
simp only [isAlphaEqvVarList_length binders xs ys h2_right] at c1
State after:
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
c2 : ¬(Y = hd.name ∧ ys.length = hd.args.length)
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
c1 : X = 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)

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
c2 : ¬(Y = hd.name ∧ ys.length = hd.args.length)
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
c1 : X = 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)
Tactic:
subst h2_left
State after:
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'
ys : List VarName
h2_right : isAlphaEqvVarList binders xs ys
c1 : X = hd.name ∧ ys.length = hd.args.length
c2 : ¬(X = 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_ X ys)

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'
ys : List VarName
h2_right : isAlphaEqvVarList binders xs ys
c1 : X = hd.name ∧ ys.length = hd.args.length
c2 : ¬(X = 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_ X ys)
Tactic:
contradiction
State after:
no goals

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
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
c2 : 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
Tactic:
cases h2
State after:
case intro
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
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
c2 : Y = hd.name ∧ ys.length = hd.args.length
left✝ : X = Y
right✝ : isAlphaEqvVarList binders xs ys
⊢ Holds D I V tl (def_ X xs) ↔ Holds D I (Function.updateListITE V' hd.args (List.map V' ys)) tl hd.q

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
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
c2 : Y = hd.name ∧ ys.length = hd.args.length
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
⊢ Holds D I V tl (def_ X xs) ↔ Holds D I (Function.updateListITE V' hd.args (List.map V' ys)) tl hd.q
Tactic:
case intro h2_left h2_right =>
  simp only [← isAlphaEqvVarList_length binders xs ys h2_right] at c2
  subst h2_left
  contradiction
State after:
no goals

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
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
c2 : Y = hd.name ∧ ys.length = hd.args.length
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
⊢ Holds D I V tl (def_ X xs) ↔ Holds D I (Function.updateListITE V' hd.args (List.map V' ys)) tl hd.q
Tactic:
simp only [← isAlphaEqvVarList_length binders xs ys h2_right] at c2
State after:
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
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
c2 : Y = hd.name ∧ xs.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

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
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
h2_left : X = Y
h2_right : isAlphaEqvVarList binders xs ys
c2 : Y = hd.name ∧ xs.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
Tactic:
subst h2_left
State after:
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'
ys : List VarName
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
h2_right : isAlphaEqvVarList binders xs ys
c2 : X = hd.name ∧ xs.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

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'
ys : List VarName
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
h2_right : isAlphaEqvVarList binders xs ys
c2 : X = hd.name ∧ xs.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
Tactic:
contradiction
State after:
no goals

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
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
c2 : ¬(Y = hd.name ∧ ys.length = hd.args.length)
⊢ Holds D I V tl (def_ X xs) ↔ Holds D I V' tl (def_ Y ys)
Tactic:
exact ih V V' (def_ X xs) (def_ Y ys) binders h1 h2
State after:
no goals