internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi.not_ → V' x = V (σ x)
h2 : ∀ x ∈ phi.not_.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E phi.not_ ↔ Holds D I V E (subAux c τ σ phi.not_)
Tactic:
simp only [isFreeIn] at h1
Proof state after:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)
h2 : ∀ x ∈ phi.not_.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E phi.not_ ↔ Holds D I V E (subAux c τ σ phi.not_)
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)
h2 : ∀ x ∈ phi.not_.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E phi.not_ ↔ Holds D I V E (subAux c τ σ phi.not_)
Tactic:
simp only [predVarSet] at h2
Proof state after:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)
h2 : ∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E phi.not_ ↔ Holds D I V E (subAux c τ σ phi.not_)
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)
h2 : ∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E phi.not_ ↔ Holds D I V E (subAux c τ σ phi.not_)
Tactic:
simp only [subAux]
Proof state after:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)
h2 : ∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E phi.not_ ↔ Holds D I V E (subAux c τ σ phi).not_
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)
h2 : ∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E phi.not_ ↔ Holds D I V E (subAux c τ σ phi).not_
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)
h2 : ∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ ¬Holds D (I' D I V'' E τ) V' E phi ↔ ¬Holds D I V E (subAux c τ σ phi)
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)
h2 : ∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ ¬Holds D (I' D I V'' E τ) V' E phi ↔ ¬Holds D I V E (subAux c τ σ phi)
Tactic:
congr! 1
Proof state after:
case a.h.e'_1.a
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)
h2 : ∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi)
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case a.h.e'_1.a
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)
h2 : ∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi)
Tactic:
exact phi_ih V V' σ h1 h2
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
psi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x psi → V' x = V (σ x)) →
      (∀ x ∈ psi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E psi ↔ Holds D I V E (subAux c τ σ psi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x (phi.iff_ psi) → V' x = V (σ x)
h2 : ∀ x ∈ (phi.iff_ psi).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E (phi.iff_ psi) ↔ Holds D I V E (subAux c τ σ (phi.iff_ psi))
Tactic:
simp only [isFreeIn] at h1
Proof state after:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
psi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x psi → V' x = V (σ x)) →
      (∀ x ∈ psi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E psi ↔ Holds D I V E (subAux c τ σ psi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi ∨ isFreeIn x psi → V' x = V (σ x)
h2 : ∀ x ∈ (phi.iff_ psi).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E (phi.iff_ psi) ↔ Holds D I V E (subAux c τ σ (phi.iff_ psi))
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
psi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x psi → V' x = V (σ x)) →
      (∀ x ∈ psi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E psi ↔ Holds D I V E (subAux c τ σ psi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi ∨ isFreeIn x psi → V' x = V (σ x)
h2 : ∀ x ∈ (phi.iff_ psi).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E (phi.iff_ psi) ↔ Holds D I V E (subAux c τ σ (phi.iff_ psi))
Tactic:
simp only [predVarSet] at h2
Proof state after:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
psi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x psi → V' x = V (σ x)) →
      (∀ x ∈ psi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E psi ↔ Holds D I V E (subAux c τ σ psi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi ∨ isFreeIn x psi → V' x = V (σ x)
h2 : ∀ x ∈ (phi.predVarSet ∪ psi.predVarSet).biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E (phi.iff_ psi) ↔ Holds D I V E (subAux c τ σ (phi.iff_ psi))
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
psi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x psi → V' x = V (σ x)) →
      (∀ x ∈ psi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E psi ↔ Holds D I V E (subAux c τ σ psi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi ∨ isFreeIn x psi → V' x = V (σ x)
h2 : ∀ x ∈ (phi.predVarSet ∪ psi.predVarSet).biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E (phi.iff_ psi) ↔ Holds D I V E (subAux c τ σ (phi.iff_ psi))
Tactic:
simp only [subAux]
Proof state after:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
psi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x psi → V' x = V (σ x)) →
      (∀ x ∈ psi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E psi ↔ Holds D I V E (subAux c τ σ psi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi ∨ isFreeIn x psi → V' x = V (σ x)
h2 : ∀ x ∈ (phi.predVarSet ∪ psi.predVarSet).biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E (phi.iff_ psi) ↔ Holds D I V E ((subAux c τ σ phi).iff_ (subAux c τ σ psi))
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
psi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x psi → V' x = V (σ x)) →
      (∀ x ∈ psi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E psi ↔ Holds D I V E (subAux c τ σ psi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi ∨ isFreeIn x psi → V' x = V (σ x)
h2 : ∀ x ∈ (phi.predVarSet ∪ psi.predVarSet).biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E (phi.iff_ psi) ↔ Holds D I V E ((subAux c τ σ phi).iff_ (subAux c τ σ psi))
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
psi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x psi → V' x = V (σ x)) →
      (∀ x ∈ psi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E psi ↔ Holds D I V E (subAux c τ σ psi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi ∨ isFreeIn x psi → V' x = V (σ x)
h2 : ∀ x ∈ (phi.predVarSet ∪ psi.predVarSet).biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D (I' D I V'' E τ) V' E psi) ↔
    (Holds D I V E (subAux c τ σ phi) ↔ Holds D I V E (subAux c τ σ psi))
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
psi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x psi → V' x = V (σ x)) →
      (∀ x ∈ psi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E psi ↔ Holds D I V E (subAux c τ σ psi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi ∨ isFreeIn x psi → V' x = V (σ x)
h2 : ∀ x ∈ (phi.predVarSet ∪ psi.predVarSet).biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D (I' D I V'' E τ) V' E psi) ↔
    (Holds D I V E (subAux c τ σ phi) ↔ Holds D I V E (subAux c τ σ psi))
Tactic:
congr! 1
Proof state after:
case a.h.e'_1.a
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
psi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x psi → V' x = V (σ x)) →
      (∀ x ∈ psi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E psi ↔ Holds D I V E (subAux c τ σ psi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi ∨ isFreeIn x psi → V' x = V (σ x)
h2 : ∀ x ∈ (phi.predVarSet ∪ psi.predVarSet).biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi)

case a.h.e'_2.a
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
psi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x psi → V' x = V (σ x)) →
      (∀ x ∈ psi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E psi ↔ Holds D I V E (subAux c τ σ psi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi ∨ isFreeIn x psi → V' x = V (σ x)
h2 : ∀ x ∈ (phi.predVarSet ∪ psi.predVarSet).biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E psi ↔ Holds D I V E (subAux c τ σ psi)
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case a.h.e'_1.a
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
psi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x psi → V' x = V (σ x)) →
      (∀ x ∈ psi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E psi ↔ Holds D I V E (subAux c τ σ psi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi ∨ isFreeIn x psi → V' x = V (σ x)
h2 : ∀ x ∈ (phi.predVarSet ∪ psi.predVarSet).biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi)
Tactic:
apply phi_ih V V' σ
Proof state after:
case a.h.e'_1.a.h1
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
psi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x psi → V' x = V (σ x)) →
      (∀ x ∈ psi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E psi ↔ Holds D I V E (subAux c τ σ psi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi ∨ isFreeIn x psi → V' x = V (σ x)
h2 : ∀ x ∈ (phi.predVarSet ∪ psi.predVarSet).biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ ∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)

case a.h.e'_1.a.h2
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi psi : Formula
phi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
psi_ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x psi → V' x = V (σ x)) →
      (∀ x ∈ psi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E psi ↔ Holds D I V E (subAux c τ σ psi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x phi ∨ isFreeIn x psi → V' x = V (σ x)
h2 : ∀ x ∈ (phi.predVarSet ∪ psi.predVarSet).biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ ∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x