internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
h1_right_left : ∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1
h1_right_right : xs.length = (τ X xs.length).1.length
s1 :
  Holds D I (Function.updateListITE V (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2)
v : VarName
a1 : isFreeIn v (τ X xs.length).2
c1 : v ∈ (τ X xs.length).1
⊢ (τ X xs.length).1.length = xs.length
Tactic:
symm
Proof state after:
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
h1_right_left : ∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1
h1_right_right : xs.length = (τ X xs.length).1.length
s1 :
  Holds D I (Function.updateListITE V (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2)
v : VarName
a1 : isFreeIn v (τ X xs.length).2
c1 : v ∈ (τ X xs.length).1
⊢ xs.length = (τ X xs.length).1.length
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
h1_right_left : ∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1
h1_right_right : xs.length = (τ X xs.length).1.length
s1 :
  Holds D I (Function.updateListITE V (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2)
v : VarName
a1 : isFreeIn v (τ X xs.length).2
c1 : v ∈ (τ X xs.length).1
⊢ xs.length = (τ X xs.length).1.length
Tactic:
exact h1_right_right
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
case neg
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
h1_right_left : ∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1
h1_right_right : xs.length = (τ X xs.length).1.length
s1 :
  Holds D I (Function.updateListITE V (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2)
v : VarName
a1 : isFreeIn v (τ X xs.length).2
c1 : v ∉ (τ X xs.length).1
⊢ Function.updateListITE V (τ X xs.length).1 (List.map V xs) v =
    Function.updateListITE V' (τ X xs.length).1 (List.map V xs) v
Tactic:
by_cases c2 : v ∈ binders
Proof state after:
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
h1_right_left : ∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1
h1_right_right : xs.length = (τ X xs.length).1.length
s1 :
  Holds D I (Function.updateListITE V (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2)
v : VarName
a1 : isFreeIn v (τ X xs.length).2
c1 : v ∉ (τ X xs.length).1
c2 : v ∈ binders
⊢ Function.updateListITE V (τ X xs.length).1 (List.map V xs) v =
    Function.updateListITE V' (τ X xs.length).1 (List.map V xs) v

case neg
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
h1_right_left : ∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1
h1_right_right : xs.length = (τ X xs.length).1.length
s1 :
  Holds D I (Function.updateListITE V (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2)
v : VarName
a1 : isFreeIn v (τ X xs.length).2
c1 : v ∉ (τ X xs.length).1
c2 : v ∉ binders
⊢ Function.updateListITE V (τ X xs.length).1 (List.map V xs) v =
    Function.updateListITE V' (τ X xs.length).1 (List.map V xs) v
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
h1_right_left : ∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1
h1_right_right : xs.length = (τ X xs.length).1.length
s1 :
  Holds D I (Function.updateListITE V (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2)
v : VarName
a1 : isFreeIn v (τ X xs.length).2
c1 : v ∉ (τ X xs.length).1
c2 : v ∈ binders
⊢ Function.updateListITE V (τ X xs.length).1 (List.map V xs) v =
    Function.updateListITE V' (τ X xs.length).1 (List.map V xs) v
Tactic:
specialize h1_right_left v c2 a1
Proof state after:
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
h1_right_right : xs.length = (τ X xs.length).1.length
s1 :
  Holds D I (Function.updateListITE V (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2)
v : VarName
a1 : isFreeIn v (τ X xs.length).2
c1 : v ∉ (τ X xs.length).1
c2 : v ∈ binders
h1_right_left : v ∈ (τ X xs.length).1
⊢ Function.updateListITE V (τ X xs.length).1 (List.map V xs) v =
    Function.updateListITE V' (τ X xs.length).1 (List.map V xs) v
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
h1_right_right : xs.length = (τ X xs.length).1.length
s1 :
  Holds D I (Function.updateListITE V (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2)
v : VarName
a1 : isFreeIn v (τ X xs.length).2
c1 : v ∉ (τ X xs.length).1
c2 : v ∈ binders
h1_right_left : v ∈ (τ X xs.length).1
⊢ Function.updateListITE V (τ X xs.length).1 (List.map V xs) v =
    Function.updateListITE V' (τ X xs.length).1 (List.map V xs) v
Tactic:
contradiction
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
case neg
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
h1_right_left : ∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1
h1_right_right : xs.length = (τ X xs.length).1.length
s1 :
  Holds D I (Function.updateListITE V (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2)
v : VarName
a1 : isFreeIn v (τ X xs.length).2
c1 : v ∉ (τ X xs.length).1
c2 : v ∉ binders
⊢ Function.updateListITE V (τ X xs.length).1 (List.map V xs) v =
    Function.updateListITE V' (τ X xs.length).1 (List.map V xs) v
Tactic:
specialize h2 v c2
Proof state after:
case neg
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
h1_right_left : ∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1
h1_right_right : xs.length = (τ X xs.length).1.length
s1 :
  Holds D I (Function.updateListITE V (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2)
v : VarName
a1 : isFreeIn v (τ X xs.length).2
c1 : v ∉ (τ X xs.length).1
c2 : v ∉ binders
h2 : V v = V' v
⊢ Function.updateListITE V (τ X xs.length).1 (List.map V xs) v =
    Function.updateListITE V' (τ X xs.length).1 (List.map V xs) v
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
case neg
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
h1_right_left : ∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1
h1_right_right : xs.length = (τ X xs.length).1.length
s1 :
  Holds D I (Function.updateListITE V (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2)
v : VarName
a1 : isFreeIn v (τ X xs.length).2
c1 : v ∉ (τ X xs.length).1
c2 : v ∉ binders
h2 : V v = V' v
⊢ Function.updateListITE V (τ X xs.length).1 (List.map V xs) v =
    Function.updateListITE V' (τ X xs.length).1 (List.map V xs) v
Tactic:
apply Function.updateListITE_mem'
Proof state after:
case neg.h1
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
h1_right_left : ∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1
h1_right_right : xs.length = (τ X xs.length).1.length
s1 :
  Holds D I (Function.updateListITE V (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2)
v : VarName
a1 : isFreeIn v (τ X xs.length).2
c1 : v ∉ (τ X xs.length).1
c2 : v ∉ binders
h2 : V v = V' v
⊢ V v = V' v
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
case neg.h1
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1_left : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
h1_right_left : ∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1
h1_right_right : xs.length = (τ X xs.length).1.length
s1 :
  Holds D I (Function.updateListITE V (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I V E (Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2)
v : VarName
a1 : isFreeIn v (τ X xs.length).2
c1 : v ∉ (τ X xs.length).1
c2 : v ∉ binders
h2 : V v = V' v
⊢ V v = V' v
Tactic:
exact h2
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
x y : VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (eq_ x y)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if ds.length = (τ X ds.length).1.length then
            Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
          else I.pred_var_ X ds }
      V E (eq_ x y) ↔
    Holds D I V E (replace τ (eq_ x y))
Tactic:
simp only [replace]
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
x y : VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (eq_ x y)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if ds.length = (τ X ds.length).1.length then
            Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
          else I.pred_var_ X ds }
      V E (eq_ x y) ↔
    Holds D I V E (eq_ x y)
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
x y : VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (eq_ x y)
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if ds.length = (τ X ds.length).1.length then
            Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
          else I.pred_var_ X ds }
      V E (eq_ x y) ↔
    Holds D I V E (eq_ x y)
Tactic:
simp only [Holds]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders false_
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if ds.length = (τ X ds.length).1.length then
            Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
          else I.pred_var_ X ds }
      V E false_ ↔
    Holds D I V E (replace τ false_)
Tactic:
simp only [replace]
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders false_
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if ds.length = (τ X ds.length).1.length then
            Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
          else I.pred_var_ X ds }
      V E false_ ↔
    Holds D I V E false_
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders false_
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if ds.length = (τ X ds.length).1.length then
            Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
          else I.pred_var_ X ds }
      V E false_ ↔
    Holds D I V E false_
Tactic:
simp only [Holds]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                if ds.length = (τ X ds.length).1.length then
                  Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders phi.not_
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if ds.length = (τ X ds.length).1.length then
            Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
          else I.pred_var_ X ds }
      V E phi.not_ ↔
    Holds D I V E (replace τ phi.not_)
Tactic:
simp only [admitsAux] at h1
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                if ds.length = (τ X ds.length).1.length then
                  Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders phi
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if ds.length = (τ X ds.length).1.length then
            Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
          else I.pred_var_ X ds }
      V E phi.not_ ↔
    Holds D I V E (replace τ phi.not_)
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                if ds.length = (τ X ds.length).1.length then
                  Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders phi
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if ds.length = (τ X ds.length).1.length then
            Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
          else I.pred_var_ X ds }
      V E phi.not_ ↔
    Holds D I V E (replace τ phi.not_)
Tactic:
simp only [replace]
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                if ds.length = (τ X ds.length).1.length then
                  Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders phi
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if ds.length = (τ X ds.length).1.length then
            Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
          else I.pred_var_ X ds }
      V E phi.not_ ↔
    Holds D I V E (replace τ phi).not_
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                if ds.length = (τ X ds.length).1.length then
                  Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders phi
h2 : ∀ x ∉ binders, V x = V' x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if ds.length = (τ X ds.length).1.length then
            Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
          else I.pred_var_ X ds }
      V E phi.not_ ↔
    Holds D I V E (replace τ phi).not_
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
phi : Formula
phi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders phi →
      (∀ x ∉ binders, V x = V' x) →
        (Holds D
            { nonempty := ⋯, pred_const_ := I.pred_const_,
              pred_var_ := fun X ds =>
                if ds.length = (τ X ds.length).1.length then
                  Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace τ phi))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders phi
h2 : ∀ x ∉ binders, V x = V' x
⊢ ¬Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun X ds =>
            if ds.length = (τ X ds.length).1.length then
              Holds D I (Function.updateListITE V' (τ X ds.length).1 ds) E (τ X ds.length).2
            else I.pred_var_ X ds }
        V E phi ↔
    ¬Holds D I V E (replace τ phi)