internlm/Lean-Github huggingface dataset:
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 ↔
    ¬Holds D I V E (replace τ phi)
Tactic:
congr! 1
Proof state after:
case a.h.e'_1.a
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)
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
case a.h.e'_1.a
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)
Tactic:
exact phi_ih V binders h1 h2
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
case a.h.e'_1.a
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
phi psi : 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))
psi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders psi →
      (∀ 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 psi ↔
          Holds D I V E (replace τ psi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : admitsAux τ binders phi
h1_right : admitsAux τ binders psi
⊢ 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)
Tactic:
exact phi_ih V binders h1_left h2
Proof state after:
no goals
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
case a.h.e'_2.a
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
phi psi : 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))
psi_ih :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders psi →
      (∀ 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 psi ↔
          Holds D I V E (replace τ psi))
V : VarAssignment D
binders : Finset VarName
h2 : ∀ x ∉ binders, V x = V' x
h1_left : admitsAux τ binders phi
h1_right : admitsAux τ binders psi
⊢ 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 psi ↔
    Holds D I V E (replace τ psi)
Tactic:
exact psi_ih V binders h1_right 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 : VarName
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 (exists_ x 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 (exists_ x phi) ↔
    Holds D I V E (replace τ (exists_ x phi))
Tactic:
simp only [admitsAux] at h1
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
x : VarName
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 ∪ {x}) 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 (exists_ x phi) ↔
    Holds D I V E (replace τ (exists_ x phi))
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 : VarName
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 ∪ {x}) 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 (exists_ x phi) ↔
    Holds D I V E (replace τ (exists_ x phi))
Tactic:
simp only [replace]
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
x : VarName
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 ∪ {x}) 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 (exists_ x phi) ↔
    Holds D I V E (exists_ x (replace τ phi))
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 : VarName
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 ∪ {x}) 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 (exists_ x phi) ↔
    Holds D I V E (exists_ x (replace τ phi))
Tactic:
simp only [Holds]
Proof state after:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
x : VarName
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 ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
⊢ (∃ d,
      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 }
        (Function.updateITE V x d) E phi) ↔
    ∃ d, Holds D I (Function.updateITE V x d) E (replace τ phi)
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 : VarName
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 ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
⊢ (∃ d,
      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 }
        (Function.updateITE V x d) E phi) ↔
    ∃ d, Holds D I (Function.updateITE V x d) E (replace τ phi)
Tactic:
first | apply forall_congr' | apply exists_congr
Proof state after:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
x : VarName
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 ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
⊢ ∀ (a : D),
    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 }
        (Function.updateITE V x a) E phi ↔
      Holds D I (Function.updateITE V x a) E (replace τ phi)
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
x : VarName
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 ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
⊢ ∀ (a : D),
    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 }
        (Function.updateITE V x a) E phi ↔
      Holds D I (Function.updateITE V x a) E (replace τ phi)
Tactic:
intro d
Proof state after:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
x : VarName
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 ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
d : D
⊢ 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 }
      (Function.updateITE V x d) E phi ↔
    Holds D I (Function.updateITE V x d) E (replace τ phi)
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
x : VarName
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 ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
d : D
⊢ 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 }
      (Function.updateITE V x d) E phi ↔
    Holds D I (Function.updateITE V x d) E (replace τ phi)
Tactic:
apply phi_ih (Function.updateITE V x d) (binders ∪ {x}) h1
Proof state after:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
x : VarName
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 ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
d : D
⊢ ∀ x_1 ∉ binders ∪ {x}, Function.updateITE V x d x_1 = V' x_1
Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux
Proof state before:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
x : VarName
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 ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
d : D
⊢ ∀ x_1 ∉ binders ∪ {x}, Function.updateITE V x d x_1 = V' x_1
Tactic:
intro v a1
Proof state after:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
x : VarName
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 ∪ {x}) phi
h2 : ∀ x ∉ binders, V x = V' x
d : D
v : VarName
a1 : v ∉ binders ∪ {x}
⊢ Function.updateITE V x d v = V' v