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
h2 : ∀ v ∉ binders, V' v = V v
h1 : v = v ∨ fastAdmitsAux v t (binders ∪ {v}) phi
⊢ (∃ d, Holds D I (Function.updateITE (Function.updateITE V v (V' t)) v d) (head✝ :: tail✝) phi) ↔
    ∃ d, Holds D I (Function.updateITE V v d) (head✝ :: tail✝) phi
Tactic:
apply exists_congr
Proof state after:
case h
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
h2 : ∀ v ∉ binders, V' v = V v
h1 : v = v ∨ fastAdmitsAux v t (binders ∪ {v}) phi
⊢ ∀ (a : D),
    Holds D I (Function.updateITE (Function.updateITE V v (V' t)) v a) (head✝ :: tail✝) phi ↔
      Holds D I (Function.updateITE V v a) (head✝ :: tail✝) phi
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
c1 : ¬v = x
⊢ (∃ d, Holds D I (Function.updateITE (Function.updateITE V v (V' t)) x d) (head✝ :: tail✝) phi) ↔
    Holds D I V (head✝ :: tail✝) (exists_ x (fastReplaceFree v t phi))
Tactic:
simp only [Holds]
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 : 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
c1 : ¬v = x
⊢ (∃ d, Holds D I (Function.updateITE (Function.updateITE V v (V' t)) x d) (head✝ :: tail✝) phi) ↔
    ∃ d, Holds D I (Function.updateITE V x d) (head✝ :: tail✝) (fastReplaceFree v t phi)
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
c1 : ¬v = x
⊢ (∃ d, Holds D I (Function.updateITE (Function.updateITE V v (V' t)) x d) (head✝ :: tail✝) phi) ↔
    ∃ d, Holds D I (Function.updateITE V x d) (head✝ :: tail✝) (fastReplaceFree v t phi)
Tactic:
first | apply forall_congr' | apply exists_congr
Proof state after:
case h
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
c1 : ¬v = x
⊢ ∀ (a : D),
    Holds D I (Function.updateITE (Function.updateITE V v (V' t)) x a) (head✝ :: tail✝) phi ↔
      Holds D I (Function.updateITE V x a) (head✝ :: tail✝) (fastReplaceFree v t phi)
Theorem: FOL.NV.Sub.Var.One.Rec.substitution_theorem_aux
Proof state before:
case h
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
c1 : ¬v = x
⊢ ∀ (a : D),
    Holds D I (Function.updateITE (Function.updateITE V v (V' t)) x a) (head✝ :: tail✝) phi ↔
      Holds D I (Function.updateITE V x a) (head✝ :: tail✝) (fastReplaceFree v t phi)
Tactic:
intro d
Proof state after:
case h
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
c1 : ¬v = x
d : D
⊢ Holds D I (Function.updateITE (Function.updateITE V v (V' t)) x d) (head✝ :: tail✝) phi ↔
    Holds D I (Function.updateITE V x d) (head✝ :: tail✝) (fastReplaceFree v t phi)
Theorem: FOL.NV.Sub.Var.One.Rec.substitution_theorem_aux
Proof state before:
case h
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
c1 : ¬v = x
d : D
⊢ Holds D I (Function.updateITE (Function.updateITE V v (V' t)) x d) (head✝ :: tail✝) phi ↔
    Holds D I (Function.updateITE V x d) (head✝ :: tail✝) (fastReplaceFree v t phi)
Tactic:
cases h1
Proof state after:
case h.inl
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
h2 : ∀ v ∉ binders, V' v = V v
c1 : ¬v = x
d : D
h✝ : v = x
⊢ Holds D I (Function.updateITE (Function.updateITE V v (V' t)) x d) (head✝ :: tail✝) phi ↔
    Holds D I (Function.updateITE V x d) (head✝ :: tail✝) (fastReplaceFree v t phi)

case h.inr
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
h2 : ∀ v ∉ binders, V' v = V v
c1 : ¬v = x
d : D
h✝ : fastAdmitsAux v t (binders ∪ {x}) phi
⊢ Holds D I (Function.updateITE (Function.updateITE V v (V' t)) x d) (head✝ :: tail✝) phi ↔
    Holds D I (Function.updateITE V x d) (head✝ :: tail✝) (fastReplaceFree v t phi)
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
h2 : ∀ v ∉ binders, V' v = V v
c1 : ¬v = x
d : D
h1 : v = x
⊢ Holds D I (Function.updateITE (Function.updateITE V v (V' t)) x d) (head✝ :: tail✝) phi ↔
    Holds D I (Function.updateITE V x d) (head✝ :: tail✝) (fastReplaceFree v t phi)
Tactic:
case inl h1 =>
  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 : 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
h2 : ∀ v ∉ binders, V' v = V v
c1 : ¬v = x
d : D
h1 : fastAdmitsAux v t (binders ∪ {x}) phi
⊢ Holds D I (Function.updateITE (Function.updateITE V v (V' t)) x d) (head✝ :: tail✝) phi ↔
    Holds D I (Function.updateITE V x d) (head✝ :: tail✝) (fastReplaceFree v t phi)
Tactic:
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:
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
c1 : ¬v = x
⊢ (∀ (d : D), Holds D I (Function.updateITE (Function.updateITE V v (V' t)) x d) (head✝ :: tail✝) phi) ↔
    ∀ (d : D), Holds D I (Function.updateITE V x d) (head✝ :: tail✝) (fastReplaceFree v t phi)
Tactic:
apply forall_congr'
Proof state after:
case h
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
c1 : ¬v = x
⊢ ∀ (a : D),
    Holds D I (Function.updateITE (Function.updateITE V v (V' t)) x a) (head✝ :: tail✝) phi ↔
      Holds D I (Function.updateITE V x a) (head✝ :: tail✝) (fastReplaceFree v t phi)
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
c1 : ¬v = x
⊢ (∃ d, Holds D I (Function.updateITE (Function.updateITE V v (V' t)) x d) (head✝ :: tail✝) phi) ↔
    ∃ d, Holds D I (Function.updateITE V x d) (head✝ :: tail✝) (fastReplaceFree v t phi)
Tactic:
apply exists_congr
Proof state after:
case h
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
c1 : ¬v = x
⊢ ∀ (a : D),
    Holds D I (Function.updateITE (Function.updateITE V v (V' t)) x a) (head✝ :: tail✝) phi ↔
      Holds D I (Function.updateITE V x a) (head✝ :: tail✝) (fastReplaceFree v t phi)
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
h2 : ∀ v ∉ binders, V' v = V v
c1 : ¬v = x
d : D
h1 : v = x
⊢ Holds D I (Function.updateITE (Function.updateITE V v (V' t)) x d) (head✝ :: tail✝) phi ↔
    Holds D I (Function.updateITE V x d) (head✝ :: tail✝) (fastReplaceFree v t phi)
Tactic:
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 : 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
h2 : ∀ v ∉ binders, V' v = V v
c1 : ¬v = x
d : D
h1 : fastAdmitsAux v t (binders ∪ {x}) phi
⊢ Holds D I (Function.updateITE (Function.updateITE V v (V' t)) x d) (head✝ :: tail✝) phi ↔
    Holds D I (Function.updateITE V x d) (head✝ :: tail✝) (fastReplaceFree v t phi)
Tactic:
simp only [Function.updateITE_comm V v x d (V' t) c1]
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 : 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
h2 : ∀ v ∉ binders, V' v = V v
c1 : ¬v = x
d : D
h1 : fastAdmitsAux v t (binders ∪ {x}) phi
⊢ Holds D I (Function.updateITE (Function.updateITE V x d) v (V' t)) (head✝ :: tail✝) phi ↔
    Holds D I (Function.updateITE V x d) (head✝ :: tail✝) (fastReplaceFree v t phi)
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
h2 : ∀ v ∉ binders, V' v = V v
c1 : ¬v = x
d : D
h1 : fastAdmitsAux v t (binders ∪ {x}) phi
⊢ Holds D I (Function.updateITE (Function.updateITE V x d) v (V' t)) (head✝ :: tail✝) phi ↔
    Holds D I (Function.updateITE V x d) (head✝ :: tail✝) (fastReplaceFree v t phi)
Tactic:
apply phi_ih (Function.updateITE V x d) (binders ∪ {x}) h1
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 : 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
h2 : ∀ v ∉ binders, V' v = V v
c1 : ¬v = x
d : D
h1 : fastAdmitsAux v t (binders ∪ {x}) phi
⊢ ∀ v ∉ binders ∪ {x}, V' v = Function.updateITE V x d v