internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Var.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h1 : fastAdmitsAux v t binders phi
h2 : ∀ v ∉ binders, V' v = V v
⊢ ¬Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
    ¬Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi)
Tactic:
case not_ phi phi_ih =>
  congr! 1
  exact phi_ih V binders h1 h2
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
x : VarName
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    fastAdmitsAux v t binders phi →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) phi ↔
          Holds D I V (head✝ :: tail✝) (fastReplaceFree v t phi))
V : VarAssignment D
binders : Finset VarName
h1 : v = x ∨ fastAdmitsAux v t (binders ∪ {x}) phi
h2 : ∀ v ∉ binders, V' v = V v
⊢ (∃ d, Holds D I (Function.updateITE (Function.updateITE V v (V' t)) x d) (head✝ :: tail✝) phi) ↔
    Holds D I V (head✝ :: tail✝) (if v = x then exists_ x phi else exists_ x (fastReplaceFree v t phi))
Tactic:
case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  split_ifs
  case _ c1 =>
    subst c1
    simp only [Holds]
    first | apply forall_congr' | apply exists_congr
    intro d
    congr! 1
    funext x
    simp only [Function.updateITE]
    split_ifs <;> rfl
  case _ c1 =>
    simp only [Holds]
    first | apply forall_congr' | apply exists_congr
    intro d
    cases h1
    case inl h1 =>
      contradiction
    case inr h1 =>
      simp only [Function.updateITE_comm V v x d (V' t) c1]
      apply phi_ih (Function.updateITE V x d) (binders ∪ {x}) h1
      simp only [Function.updateITE]
      simp
      push_neg
      intros v' a1 a2
      simp only [if_neg a2]
      exact h2 v' a1
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.substitution_theorem_aux
Proof state before:
case cons.def_
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
a✝¹ : DefName
a✝ : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : fastAdmitsAux v t binders (def_ a✝¹ a✝)
h2 : ∀ v ∉ binders, V' v = V v
⊢ Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) (def_ a✝¹ a✝) ↔
    Holds D I V (head✝ :: tail✝) (fastReplaceFree v t (def_ a✝¹ a✝))
Tactic:
simp only [fastAdmitsAux] at h1
Proof state after:
case cons.def_
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
a✝¹ : DefName
a✝ : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ a✝ → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
⊢ Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) (def_ a✝¹ a✝) ↔
    Holds D I V (head✝ :: tail✝) (fastReplaceFree v t (def_ a✝¹ a✝))
Theorem: FOL.NV.Sub.Var.One.Rec.substitution_theorem_aux
Proof state before:
case cons.def_
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
a✝¹ : DefName
a✝ : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ a✝ → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
⊢ Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) (def_ a✝¹ a✝) ↔
    Holds D I V (head✝ :: tail✝) (fastReplaceFree v t (def_ a✝¹ a✝))
Tactic:
simp only [fastReplaceFree]
Proof state after:
case cons.def_
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
a✝¹ : DefName
a✝ : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ a✝ → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
⊢ Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) (def_ a✝¹ a✝) ↔
    Holds D I V (head✝ :: tail✝) (def_ a✝¹ (List.map (fun x => if v = x then t else x) a✝))
Theorem: FOL.NV.Sub.Var.One.Rec.substitution_theorem_aux
Proof state before:
case cons.def_
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
a✝¹ : DefName
a✝ : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ a✝ → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
⊢ Holds D I (Function.updateITE V v (V' t)) (head✝ :: tail✝) (def_ a✝¹ a✝) ↔
    Holds D I V (head✝ :: tail✝) (def_ a✝¹ (List.map (fun x => if v = x then t else x) a✝))
Tactic:
simp only [Holds]
Proof state after:
case cons.def_
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
a✝¹ : DefName
a✝ : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ a✝ → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
⊢ (if a✝¹ = head✝.name ∧ a✝.length = head✝.args.length then
      Holds D I
        (Function.updateListITE (Function.updateITE V v (V' t)) head✝.args
          (List.map (Function.updateITE V v (V' t)) a✝))
        tail✝ head✝.q
    else Holds D I (Function.updateITE V v (V' t)) tail✝ (def_ a✝¹ a✝)) ↔
    if a✝¹ = head✝.name ∧ (List.map (fun x => if v = x then t else x) a✝).length = head✝.args.length then
      Holds D I (Function.updateListITE V head✝.args (List.map V (List.map (fun x => if v = x then t else x) a✝))) tail✝
        head✝.q
    else Holds D I V tail✝ (def_ a✝¹ (List.map (fun x => if v = x then t else x) a✝))
Theorem: FOL.NV.Sub.Var.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
⊢ I.pred_var_ X (List.map (Function.updateITE V v (V' t)) xs) ↔
    I.pred_var_ X (List.map V (List.map (fun x => if v = x then t else x) xs))
Tactic:
simp
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
⊢ I.pred_var_ X (List.map (Function.updateITE V v (V' t)) xs) ↔
    I.pred_var_ X (List.map (V ∘ fun x => if v = x then t else x) xs)
Theorem: FOL.NV.Sub.Var.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
⊢ I.pred_var_ X (List.map (Function.updateITE V v (V' t)) xs) ↔
    I.pred_var_ X (List.map (V ∘ fun x => if v = x then t else x) xs)
Tactic:
congr! 1
Proof state after:
case a.h.e'_4
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
⊢ List.map (Function.updateITE V v (V' t)) xs = List.map (V ∘ fun x => if v = x then t else x) xs
Theorem: FOL.NV.Sub.Var.One.Rec.substitution_theorem_aux
Proof state before:
case a.h.e'_4
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
⊢ List.map (Function.updateITE V v (V' t)) xs = List.map (V ∘ fun x => if v = x then t else x) 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
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
⊢ ∀ x ∈ xs, Function.updateITE V v (V' t) x = (V ∘ fun x => if v = x then t else x) x
Theorem: FOL.NV.Sub.Var.One.Rec.substitution_theorem_aux
Proof state before:
case a.h.e'_4
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
⊢ ∀ x ∈ xs, Function.updateITE V v (V' t) x = (V ∘ fun x => if v = x then t else x) x
Tactic:
intro x a1
Proof state after:
case a.h.e'_4
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
x : VarName
a1 : x ∈ xs
⊢ Function.updateITE V v (V' t) x = (V ∘ fun x => if v = x then t else x) x
Theorem: FOL.NV.Sub.Var.One.Rec.substitution_theorem_aux
Proof state before:
case a.h.e'_4
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
x : VarName
a1 : x ∈ xs
⊢ Function.updateITE V v (V' t) x = (V ∘ fun x => if v = x then t else x) x
Tactic:
simp
Proof state after:
case a.h.e'_4
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
x : VarName
a1 : x ∈ xs
⊢ Function.updateITE V v (V' t) x = V (if v = x then t else x)
Theorem: FOL.NV.Sub.Var.One.Rec.substitution_theorem_aux
Proof state before:
case a.h.e'_4
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
x : VarName
a1 : x ∈ xs
⊢ Function.updateITE V v (V' t) x = V (if v = x then t else x)
Tactic:
simp only [Function.updateITE]
Proof state after:
case a.h.e'_4
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
x : VarName
a1 : x ∈ xs
⊢ (if x = v then V' t else V x) = V (if v = x then t else x)
Theorem: FOL.NV.Sub.Var.One.Rec.substitution_theorem_aux
Proof state before:
case a.h.e'_4
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
x : VarName
a1 : x ∈ xs
⊢ (if x = v then V' t else V x) = V (if v = x then t else x)
Tactic:
split_ifs
Proof state after:
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
x : VarName
a1 : x ∈ xs
h✝¹ : x = v
h✝ : v = x
⊢ V' t = V t

case neg
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
x : VarName
a1 : x ∈ xs
h✝¹ : x = v
h✝ : ¬v = x
⊢ V' t = V x

case pos
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
x : VarName
a1 : x ∈ xs
h✝¹ : ¬x = v
h✝ : v = x
⊢ V x = V t

case neg
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
x : VarName
a1 : x ∈ xs
h✝¹ : ¬x = v
h✝ : ¬v = x
⊢ V x = V x
Theorem: FOL.NV.Sub.Var.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
x : VarName
a1 : x ∈ xs
c1 : x = v
c2 : v = x
⊢ V' t = V t
Tactic:
case _ c1 c2 =>
  subst c1
  tauto
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
x : VarName
a1 : x ∈ xs
c1 : x = v
c2 : ¬v = x
⊢ V' t = V x
Tactic:
case _ c1 c2 =>
  subst c1
  contradiction
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
x : VarName
a1 : x ∈ xs
c1 : ¬x = v
c2 : v = x
⊢ V x = V t
Tactic:
case _ c1 c2 =>
  subst c2
  contradiction
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
x : VarName
a1 : x ∈ xs
c1 : ¬x = v
c2 : ¬v = x
⊢ V x = V x
Tactic:
case _ c1 c2 =>
  rfl
Proof state after:
no goals
Theorem: FOL.NV.Sub.Var.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
v t : VarName
head✝ : Definition
tail✝ : List Definition
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux v t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V v (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree v t F))
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : v ∈ xs → t ∉ binders
h2 : ∀ v ∉ binders, V' v = V v
x : VarName
a1 : x ∈ xs
c1 : x = v
c2 : v = x
⊢ V' t = V t
Tactic:
subst c1
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
t : VarName
head✝ : Definition
tail✝ : List Definition
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
x : VarName
a1 : x ∈ xs
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux x t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V x (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree x t F))
h1 : x ∈ xs → t ∉ binders
c2 : x = x
⊢ V' t = V t
Theorem: FOL.NV.Sub.Var.One.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
t : VarName
head✝ : Definition
tail✝ : List Definition
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ v ∉ binders, V' v = V v
x : VarName
a1 : x ∈ xs
tail_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName) (F : Formula),
    fastAdmitsAux x t binders F →
      (∀ v ∉ binders, V' v = V v) →
        (Holds D I (Function.updateITE V x (V' t)) tail✝ F ↔ Holds D I V tail✝ (fastReplaceFree x t F))
h1 : x ∈ xs → t ∉ binders
c2 : x = x
⊢ V' t = V t
Tactic:
tauto
Proof state after:
no goals