Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case s1
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
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_1 : VarName), ¬x_1 = x ∧ isFreeIn x_1 phi → V' x_1 = V (σ x_1)
h2 : ∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
d : D
v : VarName
a1 : v ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ)
c1_left : x ∉ Finset.image (Function.updateITE σ x x) phi.freeVarSet
c1_right : x ∉ phi.predVarSet.biUnion (predVarFreeVarSet τ)
contra : v = x
⊢ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ)

D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
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_1 : VarName), ¬x_1 = x ∧ isFreeIn x_1 phi → V' x_1 = V (σ x_1)
h2 : ∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
d : D
v : VarName
a1 : v ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ)
c1_left : x ∉ Finset.image (Function.updateITE σ x x) phi.freeVarSet
c1_right : x ∉ phi.predVarSet.biUnion (predVarFreeVarSet τ)
s1 : ¬v = x
⊢ V'' v = Function.updateITE V x d v
Tactic:
subst contra
Proof state after:
case s1
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
phi : Formula
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
h2 : ∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
d : D
v : VarName
a1 : v ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ)
h1 : ∀ (x : VarName), ¬x = v ∧ isFreeIn x phi → V' x = V (σ x)
c1_left : v ∉ Finset.image (Function.updateITE σ v v) phi.freeVarSet
c1_right : v ∉ phi.predVarSet.biUnion (predVarFreeVarSet τ)
⊢ v ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ)

D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
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_1 : VarName), ¬x_1 = x ∧ isFreeIn x_1 phi → V' x_1 = V (σ x_1)
h2 : ∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
d : D
v : VarName
a1 : v ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ)
c1_left : x ∉ Finset.image (Function.updateITE σ x x) phi.freeVarSet
c1_right : x ∉ phi.predVarSet.biUnion (predVarFreeVarSet τ)
s1 : ¬v = x
⊢ V'' v = Function.updateITE V x d v