internlm/Lean-Github huggingface dataset:
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.iff_ psi) ↔ Holds D I V' (head✝ :: tail✝) (phi'.iff_ psi')
Tactic:
simp only [Holds]
Proof state after:
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')
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
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'
Tactic:
exact phi_ih V V' phi' binders h1 h2_left
Proof state after:
no goals
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
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'
Tactic:
exact psi_ih V V' psi' binders h1 h2_right
Proof state after:
no goals
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')
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'
⊢ Holds D I V (head✝ :: tail✝) (exists_ x phi) ↔ Holds D I V' (head✝ :: tail✝) (exists_ y phi')
Tactic:
simp only [Holds]
Proof state after:
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, Holds D I (Function.updateITE V x d) (head✝ :: tail✝) phi) ↔
    ∃ d, Holds D I (Function.updateITE V' y d) (head✝ :: tail✝) phi'
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')
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, Holds D I (Function.updateITE V x d) (head✝ :: tail✝) phi) ↔
    ∃ d, Holds D I (Function.updateITE V' y d) (head✝ :: tail✝) phi'
Tactic:
first | apply forall_congr' | apply exists_congr
Proof state after:
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'
⊢ ∀ (a : D),
    Holds D I (Function.updateITE V x a) (head✝ :: tail✝) phi ↔
      Holds D I (Function.updateITE V' y a) (head✝ :: tail✝) phi'
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
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'
⊢ ∀ (a : D),
    Holds D I (Function.updateITE V x a) (head✝ :: tail✝) phi ↔
      Holds D I (Function.updateITE V' y a) (head✝ :: tail✝) phi'
Tactic:
intro d
Proof state after:
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'
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof state before:
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'
Tactic:
induction h1
Proof state after:
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'
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')
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) ↔
    ∀ (d : D), Holds D I (Function.updateITE V' y d) (head✝ :: tail✝) phi'
Tactic:
apply forall_congr'
Proof state after:
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'
⊢ ∀ (a : D),
    Holds D I (Function.updateITE V x a) (head✝ :: tail✝) phi ↔
      Holds D I (Function.updateITE V' y a) (head✝ :: tail✝) phi'
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')
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, Holds D I (Function.updateITE V x d) (head✝ :: tail✝) phi) ↔
    ∃ d, Holds D I (Function.updateITE V' y d) (head✝ :: tail✝) phi'
Tactic:
apply exists_congr
Proof state after:
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'
⊢ ∀ (a : D),
    Holds D I (Function.updateITE V x a) (head✝ :: tail✝) phi ↔
      Holds D I (Function.updateITE V' y a) (head✝ :: tail✝) phi'
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_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
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_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)
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof 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
Proof state after:
no goals
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof 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
Proof state after:
no goals
Theorem: FOL.NV.isAlphaEqv_Holds_aux
Proof 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
Proof state after:
no goals