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))
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:
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 : 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
h✝ : 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 phi)

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 : 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
h✝ : ¬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))
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 phi)
Tactic:
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
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, 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:
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:
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 phi)
Tactic:
subst 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))
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) ↔
    Holds D I V (head✝ :: tail✝) (exists_ v 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))
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) ↔
    Holds D I V (head✝ :: tail✝) (exists_ v 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))
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
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:
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))
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:
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
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))
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 : D
⊢ Holds D I (Function.updateITE (Function.updateITE V v (V' t)) v d) (head✝ :: tail✝) phi ↔
    Holds D I (Function.updateITE V v d) (head✝ :: tail✝) 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))
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 : D
⊢ Holds D I (Function.updateITE (Function.updateITE V v (V' t)) v d) (head✝ :: tail✝) phi ↔
    Holds D I (Function.updateITE V v d) (head✝ :: tail✝) phi
Tactic:
congr! 1
Proof state after:
case h.a.h.e'_3
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 : D
⊢ Function.updateITE (Function.updateITE V v (V' t)) v d = Function.updateITE V v d
Theorem: FOL.NV.Sub.Var.One.Rec.substitution_theorem_aux
Proof state before:
case h.a.h.e'_3
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 : D
⊢ Function.updateITE (Function.updateITE V v (V' t)) v d = Function.updateITE V v d
Tactic:
funext x
Proof state after:
case h.a.h.e'_3.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
d : D
x : VarName
⊢ Function.updateITE (Function.updateITE V v (V' t)) v d x = Function.updateITE V v d x
Theorem: FOL.NV.Sub.Var.One.Rec.substitution_theorem_aux
Proof state before:
case h.a.h.e'_3.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
d : D
x : VarName
⊢ Function.updateITE (Function.updateITE V v (V' t)) v d x = Function.updateITE V v d x
Tactic:
simp only [Function.updateITE]
Proof state after:
case h.a.h.e'_3.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
d : D
x : VarName
⊢ (if x = v then d else if x = v then V' t else V x) = if x = v then d else V x
Theorem: FOL.NV.Sub.Var.One.Rec.substitution_theorem_aux
Proof state before:
case h.a.h.e'_3.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
d : D
x : VarName
⊢ (if x = v then d else if x = v then V' t else V x) = if x = v then d else V x
Tactic:
split_ifs <;> 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))
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 : D), Holds D I (Function.updateITE (Function.updateITE V v (V' t)) v d) (head✝ :: tail✝) phi) ↔
    ∀ (d : D), Holds D I (Function.updateITE V v d) (head✝ :: tail✝) 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))
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