internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case a.h.e'_4
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 :
  ∀
    x ∈
      if h : (τ X xs.length).isSome = true then
        ((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset
      else ∅,
    V'' x = V x
c1 : (τ X xs.length).isSome = true
c2 : ¬xs.length = ((τ X xs.length).get ⋯).1.length
x : VarName
a1 : x ∈ xs
⊢ V' x = (V ∘ σ) x
Tactic:
simp
Proof state after:
case a.h.e'_4
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 :
  ∀
    x ∈
      if h : (τ X xs.length).isSome = true then
        ((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset
      else ∅,
    V'' x = V x
c1 : (τ X xs.length).isSome = true
c2 : ¬xs.length = ((τ X xs.length).get ⋯).1.length
x : VarName
a1 : x ∈ xs
⊢ V' x = V (σ x)
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case a.h.e'_4
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 :
  ∀
    x ∈
      if h : (τ X xs.length).isSome = true then
        ((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset
      else ∅,
    V'' x = V x
c1 : (τ X xs.length).isSome = true
c2 : ¬xs.length = ((τ X xs.length).get ⋯).1.length
x : VarName
a1 : x ∈ xs
⊢ V' x = V (σ x)
Tactic:
exact h1 x a1
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)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 :
  ∀
    x ∈
      if h : (τ X xs.length).isSome = true then
        ((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset
      else ∅,
    V'' x = V x
c1 : ¬(τ X xs.length).isSome = true
⊢ I.pred_var_ X (List.map V' xs) ↔ Holds D I V E (pred_var_ X (List.map σ xs))
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 :
  ∀
    x ∈
      if h : (τ X xs.length).isSome = true then
        ((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset
      else ∅,
    V'' x = V x
c1 : ¬(τ X xs.length).isSome = true
⊢ I.pred_var_ X (List.map V' xs) ↔ I.pred_var_ X (List.map V (List.map σ xs))
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)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 :
  ∀
    x ∈
      if h : (τ X xs.length).isSome = true then
        ((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset
      else ∅,
    V'' x = V x
c1 : ¬(τ X xs.length).isSome = true
⊢ I.pred_var_ X (List.map V' xs) ↔ I.pred_var_ X (List.map V (List.map σ xs))
Tactic:
simp
Proof state after:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 :
  ∀
    x ∈
      if h : (τ X xs.length).isSome = true then
        ((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset
      else ∅,
    V'' x = V x
c1 : ¬(τ X xs.length).isSome = true
⊢ I.pred_var_ X (List.map V' xs) ↔ I.pred_var_ X (List.map (V ∘ σ) xs)
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)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 :
  ∀
    x ∈
      if h : (τ X xs.length).isSome = true then
        ((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset
      else ∅,
    V'' x = V x
c1 : ¬(τ X xs.length).isSome = true
⊢ I.pred_var_ X (List.map V' xs) ↔ I.pred_var_ X (List.map (V ∘ σ) xs)
Tactic:
congr! 1
Proof state after:
case a.h.e'_4
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 :
  ∀
    x ∈
      if h : (τ X xs.length).isSome = true then
        ((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset
      else ∅,
    V'' x = V x
c1 : ¬(τ X xs.length).isSome = true
⊢ List.map V' xs = List.map (V ∘ σ) xs
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case a.h.e'_4
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 :
  ∀
    x ∈
      if h : (τ X xs.length).isSome = true then
        ((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset
      else ∅,
    V'' x = V x
c1 : ¬(τ X xs.length).isSome = true
⊢ List.map V' xs = List.map (V ∘ σ) xs
Tactic:
simp only [List.map_eq_map_iff]
Proof state after:
case a.h.e'_4
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 :
  ∀
    x ∈
      if h : (τ X xs.length).isSome = true then
        ((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset
      else ∅,
    V'' x = V x
c1 : ¬(τ X xs.length).isSome = true
⊢ ∀ x ∈ xs, V' x = (V ∘ σ) x
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case a.h.e'_4
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 :
  ∀
    x ∈
      if h : (τ X xs.length).isSome = true then
        ((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset
      else ∅,
    V'' x = V x
c1 : ¬(τ X xs.length).isSome = true
⊢ ∀ x ∈ xs, V' x = (V ∘ σ) x
Tactic:
intro x a1
Proof state after:
case a.h.e'_4
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 :
  ∀
    x ∈
      if h : (τ X xs.length).isSome = true then
        ((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset
      else ∅,
    V'' x = V x
c1 : ¬(τ X xs.length).isSome = true
x : VarName
a1 : x ∈ xs
⊢ V' x = (V ∘ σ) x
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case a.h.e'_4
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 :
  ∀
    x ∈
      if h : (τ X xs.length).isSome = true then
        ((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset
      else ∅,
    V'' x = V x
c1 : ¬(τ X xs.length).isSome = true
x : VarName
a1 : x ∈ xs
⊢ V' x = (V ∘ σ) x
Tactic:
simp
Proof state after:
case a.h.e'_4
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 :
  ∀
    x ∈
      if h : (τ X xs.length).isSome = true then
        ((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset
      else ∅,
    V'' x = V x
c1 : ¬(τ X xs.length).isSome = true
x : VarName
a1 : x ∈ xs
⊢ V' x = V (σ x)
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case a.h.e'_4
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ x ∈ xs, V' x = V (σ x)
h2 :
  ∀
    x ∈
      if h : (τ X xs.length).isSome = true then
        ((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset
      else ∅,
    V'' x = V x
c1 : ¬(τ X xs.length).isSome = true
x : VarName
a1 : x ∈ xs
⊢ V' x = V (σ x)
Tactic:
exact h1 x a1
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)
x y : VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), isFreeIn x_1 (eq_ x y) → V' x_1 = V (σ x_1)
h2 : ∀ x_1 ∈ (eq_ x y).predVarSet.biUnion (predVarFreeVarSet τ), V'' x_1 = V x_1
⊢ Holds D (I' D I V'' E τ) V' E (eq_ x y) ↔ Holds D I V E (subAux c τ σ (eq_ x y))
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)
x y : VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), x_1 = x ∨ x_1 = y → V' x_1 = V (σ x_1)
h2 : ∀ x_1 ∈ (eq_ x y).predVarSet.biUnion (predVarFreeVarSet τ), V'' x_1 = V x_1
⊢ Holds D (I' D I V'' E τ) V' E (eq_ x y) ↔ Holds D I V E (subAux c τ σ (eq_ x y))
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)
x y : VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), x_1 = x ∨ x_1 = y → V' x_1 = V (σ x_1)
h2 : ∀ x_1 ∈ (eq_ x y).predVarSet.biUnion (predVarFreeVarSet τ), V'' x_1 = V x_1
⊢ Holds D (I' D I V'' E τ) V' E (eq_ x y) ↔ Holds D I V E (subAux c τ σ (eq_ x y))
Tactic:
simp only [subAux]
Proof state after:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x y : VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), x_1 = x ∨ x_1 = y → V' x_1 = V (σ x_1)
h2 : ∀ x_1 ∈ (eq_ x y).predVarSet.biUnion (predVarFreeVarSet τ), V'' x_1 = V x_1
⊢ Holds D (I' D I V'' E τ) V' E (eq_ x y) ↔ Holds D I V E (eq_ (σ x) (σ y))
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)
x y : VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), x_1 = x ∨ x_1 = y → V' x_1 = V (σ x_1)
h2 : ∀ x_1 ∈ (eq_ x y).predVarSet.biUnion (predVarFreeVarSet τ), V'' x_1 = V x_1
⊢ Holds D (I' D I V'' E τ) V' E (eq_ x y) ↔ Holds D I V E (eq_ (σ x) (σ y))
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x y : VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), x_1 = x ∨ x_1 = y → V' x_1 = V (σ x_1)
h2 : ∀ x_1 ∈ (eq_ x y).predVarSet.biUnion (predVarFreeVarSet τ), V'' x_1 = V x_1
⊢ V' x = V' y ↔ V (σ x) = V (σ y)
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)
x y : VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), x_1 = x ∨ x_1 = y → V' x_1 = V (σ x_1)
h2 : ∀ x_1 ∈ (eq_ x y).predVarSet.biUnion (predVarFreeVarSet τ), V'' x_1 = V x_1
⊢ V' x = V' y ↔ V (σ x) = V (σ y)
Tactic:
have s1 : V' x = V (σ x)
Proof state after:
case s1
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x y : VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), x_1 = x ∨ x_1 = y → V' x_1 = V (σ x_1)
h2 : ∀ x_1 ∈ (eq_ x y).predVarSet.biUnion (predVarFreeVarSet τ), V'' x_1 = V x_1
⊢ V' x = V (σ x)

D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x y : VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), x_1 = x ∨ x_1 = y → V' x_1 = V (σ x_1)
h2 : ∀ x_1 ∈ (eq_ x y).predVarSet.biUnion (predVarFreeVarSet τ), V'' x_1 = V x_1
s1 : V' x = V (σ x)
⊢ V' x = V' y ↔ V (σ x) = V (σ y)
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 y : VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), x_1 = x ∨ x_1 = y → V' x_1 = V (σ x_1)
h2 : ∀ x_1 ∈ (eq_ x y).predVarSet.biUnion (predVarFreeVarSet τ), V'' x_1 = V x_1
⊢ V' x = V (σ x)

D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x y : VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), x_1 = x ∨ x_1 = y → V' x_1 = V (σ x_1)
h2 : ∀ x_1 ∈ (eq_ x y).predVarSet.biUnion (predVarFreeVarSet τ), V'' x_1 = V x_1
s1 : V' x = V (σ x)
⊢ V' x = V' y ↔ V (σ x) = V (σ y)
Tactic:
apply h1
Proof state after:
case s1.a
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x y : VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), x_1 = x ∨ x_1 = y → V' x_1 = V (σ x_1)
h2 : ∀ x_1 ∈ (eq_ x y).predVarSet.biUnion (predVarFreeVarSet τ), V'' x_1 = V x_1
⊢ x = x ∨ x = y

D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x y : VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), x_1 = x ∨ x_1 = y → V' x_1 = V (σ x_1)
h2 : ∀ x_1 ∈ (eq_ x y).predVarSet.biUnion (predVarFreeVarSet τ), V'' x_1 = V x_1
s1 : V' x = V (σ x)
⊢ V' x = V' y ↔ V (σ x) = V (σ y)
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case s1.a
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x y : VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), x_1 = x ∨ x_1 = y → V' x_1 = V (σ x_1)
h2 : ∀ x_1 ∈ (eq_ x y).predVarSet.biUnion (predVarFreeVarSet τ), V'' x_1 = V x_1
⊢ x = x ∨ x = y

D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x y : VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), x_1 = x ∨ x_1 = y → V' x_1 = V (σ x_1)
h2 : ∀ x_1 ∈ (eq_ x y).predVarSet.biUnion (predVarFreeVarSet τ), V'' x_1 = V x_1
s1 : V' x = V (σ x)
⊢ V' x = V' y ↔ V (σ x) = V (σ y)
Tactic:
simp
Proof state after:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x y : VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), x_1 = x ∨ x_1 = y → V' x_1 = V (σ x_1)
h2 : ∀ x_1 ∈ (eq_ x y).predVarSet.biUnion (predVarFreeVarSet τ), V'' x_1 = V x_1
s1 : V' x = V (σ x)
⊢ V' x = V' y ↔ V (σ x) = V (σ y)
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)
x y : VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), x_1 = x ∨ x_1 = y → V' x_1 = V (σ x_1)
h2 : ∀ x_1 ∈ (eq_ x y).predVarSet.biUnion (predVarFreeVarSet τ), V'' x_1 = V x_1
s1 : V' x = V (σ x)
⊢ V' x = V' y ↔ V (σ x) = V (σ y)
Tactic:
simp only [s1]
Proof state after:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x y : VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), x_1 = x ∨ x_1 = y → V' x_1 = V (σ x_1)
h2 : ∀ x_1 ∈ (eq_ x y).predVarSet.biUnion (predVarFreeVarSet τ), V'' x_1 = V x_1
s1 : V' x = V (σ x)
⊢ V (σ x) = V' y ↔ V (σ x) = V (σ y)
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)
x y : VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), x_1 = x ∨ x_1 = y → V' x_1 = V (σ x_1)
h2 : ∀ x_1 ∈ (eq_ x y).predVarSet.biUnion (predVarFreeVarSet τ), V'' x_1 = V x_1
s1 : V' x = V (σ x)
⊢ V (σ x) = V' y ↔ V (σ x) = V (σ y)
Tactic:
have s2 : V' y = V (σ y)
Proof state after:
case s2
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x y : VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), x_1 = x ∨ x_1 = y → V' x_1 = V (σ x_1)
h2 : ∀ x_1 ∈ (eq_ x y).predVarSet.biUnion (predVarFreeVarSet τ), V'' x_1 = V x_1
s1 : V' x = V (σ x)
⊢ V' y = V (σ y)

D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x y : VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), x_1 = x ∨ x_1 = y → V' x_1 = V (σ x_1)
h2 : ∀ x_1 ∈ (eq_ x y).predVarSet.biUnion (predVarFreeVarSet τ), V'' x_1 = V x_1
s1 : V' x = V (σ x)
s2 : V' y = V (σ y)
⊢ V (σ x) = V' y ↔ V (σ x) = V (σ y)
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case s2
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x y : VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), x_1 = x ∨ x_1 = y → V' x_1 = V (σ x_1)
h2 : ∀ x_1 ∈ (eq_ x y).predVarSet.biUnion (predVarFreeVarSet τ), V'' x_1 = V x_1
s1 : V' x = V (σ x)
⊢ V' y = V (σ y)

D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x y : VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), x_1 = x ∨ x_1 = y → V' x_1 = V (σ x_1)
h2 : ∀ x_1 ∈ (eq_ x y).predVarSet.biUnion (predVarFreeVarSet τ), V'' x_1 = V x_1
s1 : V' x = V (σ x)
s2 : V' y = V (σ y)
⊢ V (σ x) = V' y ↔ V (σ x) = V (σ y)
Tactic:
apply h1
Proof state after:
case s2.a
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x y : VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), x_1 = x ∨ x_1 = y → V' x_1 = V (σ x_1)
h2 : ∀ x_1 ∈ (eq_ x y).predVarSet.biUnion (predVarFreeVarSet τ), V'' x_1 = V x_1
s1 : V' x = V (σ x)
⊢ y = x ∨ y = y

D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x y : VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), x_1 = x ∨ x_1 = y → V' x_1 = V (σ x_1)
h2 : ∀ x_1 ∈ (eq_ x y).predVarSet.biUnion (predVarFreeVarSet τ), V'' x_1 = V x_1
s1 : V' x = V (σ x)
s2 : V' y = V (σ y)
⊢ V (σ x) = V' y ↔ V (σ x) = V (σ y)
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
case s2.a
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x y : VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), x_1 = x ∨ x_1 = y → V' x_1 = V (σ x_1)
h2 : ∀ x_1 ∈ (eq_ x y).predVarSet.biUnion (predVarFreeVarSet τ), V'' x_1 = V x_1
s1 : V' x = V (σ x)
⊢ y = x ∨ y = y

D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x y : VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), x_1 = x ∨ x_1 = y → V' x_1 = V (σ x_1)
h2 : ∀ x_1 ∈ (eq_ x y).predVarSet.biUnion (predVarFreeVarSet τ), V'' x_1 = V x_1
s1 : V' x = V (σ x)
s2 : V' y = V (σ y)
⊢ V (σ x) = V' y ↔ V (σ x) = V (σ y)
Tactic:
simp
Proof state after:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x y : VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), x_1 = x ∨ x_1 = y → V' x_1 = V (σ x_1)
h2 : ∀ x_1 ∈ (eq_ x y).predVarSet.biUnion (predVarFreeVarSet τ), V'' x_1 = V x_1
s1 : V' x = V (σ x)
s2 : V' y = V (σ y)
⊢ V (σ x) = V' y ↔ V (σ x) = V (σ y)
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)
x y : VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), x_1 = x ∨ x_1 = y → V' x_1 = V (σ x_1)
h2 : ∀ x_1 ∈ (eq_ x y).predVarSet.biUnion (predVarFreeVarSet τ), V'' x_1 = V x_1
s1 : V' x = V (σ x)
s2 : V' y = V (σ y)
⊢ V (σ x) = V' y ↔ V (σ x) = V (σ y)
Tactic:
simp only [s2]
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)
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x false_ → V' x = V (σ x)
h2 : ∀ x ∈ false_.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E false_ ↔ Holds D I V E (subAux c τ σ false_)
Tactic:
simp only [subAux]
Proof state after:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x false_ → V' x = V (σ x)
h2 : ∀ x ∈ false_.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E false_ ↔ Holds D I V E false_
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)
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x false_ → V' x = V (σ x)
h2 : ∀ x ∈ false_.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E false_ ↔ Holds D I V E false_
Tactic:
simp only [Holds]
Proof state after:
no goals