internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.substitution_theorem_aux
Proof state before:
case neg.a
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
c3 : v ∉ zs
contra : v ∈ binders
a1 : v ∈ ((τ X xs.length).get ⋯).2.freeVarSet
⊢ False
Tactic:
simp only [Finset.eq_empty_iff_forall_not_mem] at h1
Proof state after:
case neg.a
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
c3 : v ∉ zs
contra : v ∈ binders
a1 : v ∈ ((τ X xs.length).get ⋯).2.freeVarSet
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      ∀ (x : VarName), x ∉ binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset)
  else True
⊢ False
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.substitution_theorem_aux
Proof state before:
case neg.a
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
c3 : v ∉ zs
contra : v ∈ binders
a1 : v ∈ ((τ X xs.length).get ⋯).2.freeVarSet
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      ∀ (x : VarName), x ∉ binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset)
  else True
⊢ False
Tactic:
simp only [c1] at h1
Proof state after:
case neg.a
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
c3 : v ∉ zs
contra : v ∈ binders
a1 : v ∈ ((τ X xs.length).get ⋯).2.freeVarSet
h1 :
  if h : True then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      ∀ (x : VarName), x ∉ binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset)
  else True
⊢ False
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.substitution_theorem_aux
Proof state before:
case neg.a
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
c3 : v ∉ zs
contra : v ∈ binders
a1 : v ∈ ((τ X xs.length).get ⋯).2.freeVarSet
h1 :
  if h : True then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      ∀ (x : VarName), x ∉ binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset)
  else True
⊢ False
Tactic:
simp only [← c2] at h1
Proof state after:
case neg.a
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
c3 : v ∉ zs
contra : v ∈ binders
a1 : v ∈ ((τ X xs.length).get ⋯).2.freeVarSet
h1 :
  if h : True then
    True → ∀ (x : VarName), x ∉ binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset)
  else True
⊢ False
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.substitution_theorem_aux
Proof state before:
case neg.a
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
c3 : v ∉ zs
contra : v ∈ binders
a1 : v ∈ ((τ X xs.length).get ⋯).2.freeVarSet
h1 :
  if h : True then
    True → ∀ (x : VarName), x ∉ binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset)
  else True
⊢ False
Tactic:
simp at h1
Proof state after:
case neg.a
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
c3 : v ∉ zs
contra : v ∈ binders
a1 : v ∈ ((τ X xs.length).get ⋯).2.freeVarSet
h1 : ∀ x ∈ binders, x ∈ ((τ X xs.length).get ⋯).2.freeVarSet → x ∈ ((τ X xs.length).get ⋯).1
⊢ False
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.substitution_theorem_aux
Proof state before:
case neg.a
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
c3 : v ∉ zs
contra : v ∈ binders
a1 : v ∈ ((τ X xs.length).get ⋯).2.freeVarSet
h1 : ∀ x ∈ binders, x ∈ ((τ X xs.length).get ⋯).2.freeVarSet → x ∈ ((τ X xs.length).get ⋯).1
⊢ False
Tactic:
specialize h1 v contra a1
Proof state after:
case neg.a
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
c3 : v ∉ zs
contra : v ∈ binders
a1 : v ∈ ((τ X xs.length).get ⋯).2.freeVarSet
h1 : v ∈ ((τ X xs.length).get ⋯).1
⊢ False
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.substitution_theorem_aux
Proof state before:
case neg.a
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
c1 : (τ X xs.length).isSome = true
c2 : xs.length = ((τ X xs.length).get ⋯).1.length
opt : Option (List VarName × Formula) := τ X xs.length
val : List VarName × Formula := opt.get c1
zs : List VarName := val.1
H : Formula := val.2
s1 :
  Holds D I V E (Var.All.Rec.Fresh.sub (Function.updateListITE id zs xs) c H) ↔
    Holds D I (Function.updateListITE V zs (List.map V xs)) E H
v : VarName
c3 : v ∉ zs
contra : v ∈ binders
a1 : v ∈ ((τ X xs.length).get ⋯).2.freeVarSet
h1 : v ∈ ((τ X xs.length).get ⋯).1
⊢ False
Tactic:
contradiction
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : (τ X xs.length).isSome = true
c2 : ¬xs.length = ((τ X xs.length).get ⋯).1.length
⊢ I.pred_var_ X (List.map V xs) ↔ Holds D I V E (pred_var_ X xs)
Tactic:
simp only [Holds]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
X : PredName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V' x = V x
h1 :
  if h : (τ X xs.length).isSome = true then
    xs.length = ((τ X xs.length).get ⋯).1.length →
      binders ∩ (((τ X xs.length).get ⋯).2.freeVarSet \ ((τ X xs.length).get ⋯).1.toFinset) = ∅
  else True
c1 : ¬(τ X xs.length).isSome = true
⊢ I.pred_var_ X (List.map V xs) ↔ Holds D I V E (pred_var_ X xs)
Tactic:
simp only [Holds]
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x y : VarName
V : 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 =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E (eq_ x y) ↔
    Holds D I V E (replace c τ (eq_ x y))
Tactic:
simp only [replace]
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (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 h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          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.Option.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x y : VarName
V : 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 h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          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.Option.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (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 =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E false_ ↔
    Holds D I V E (replace c τ false_)
Tactic:
simp only [replace]
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (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 h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E false_ ↔
    Holds D I V E false_
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (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 h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          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.Option.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (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 =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ 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 =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E phi.not_ ↔
    Holds D I V E (replace c τ phi.not_)
Tactic:
simp only [admitsAux] at h1
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (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 =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ 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 =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E phi.not_ ↔
    Holds D I V E (replace c τ phi.not_)
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (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 =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ 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 =>
          let opt := τ X ds.length;
          if h : opt.isSome = true then
            let val := opt.get h;
            let zs := val.1;
            let H := val.2;
            if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E phi.not_ ↔
    Holds D I V E (replace c τ phi.not_)
Tactic:
simp only [replace]
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (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 =>
                let opt := τ X ds.length;
                if h : opt.isSome = true then
                  let val := opt.get h;
                  let zs := val.1;
                  let H := val.2;
                  if ds.length = zs.length then Holds D I (Function.updateListITE V' zs ds) E H else I.pred_var_ X ds
                else I.pred_var_ X ds }
            V E phi ↔
          Holds D I V E (replace c τ 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 h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V E phi.not_ ↔
    Holds D I V E (replace c τ phi).not_