internlm/Lean-Github huggingface dataset:
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.substitution_theorem_aux
Proof state before:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (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 =>
                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 ∪ {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 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 }
        (Function.updateITE V x a) E phi ↔
      Holds D I (Function.updateITE V x a) E (replace c τ phi)
Tactic:
intro d
Proof state after:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (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 =>
                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 ∪ {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 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 }
      (Function.updateITE V x d) E phi ↔
    Holds D I (Function.updateITE V x d) E (replace c τ phi)
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.substitution_theorem_aux
Proof state before:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (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 =>
                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 ∪ {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 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 }
      (Function.updateITE V x d) E phi ↔
    Holds D I (Function.updateITE V x d) E (replace c τ 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
c : Char
τ : PredName → ℕ → Option (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 =>
                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 ∪ {x}) phi
h2 : ∀ x ∉ binders, V' x = V x
d : D
⊢ ∀ x_1 ∉ binders ∪ {x}, V' x_1 = Function.updateITE V x d x_1
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.substitution_theorem_aux
Proof state before:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (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 =>
                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 ∪ {x}) phi
h2 : ∀ x ∉ binders, V' x = V x
d : D
⊢ ∀ x_1 ∉ binders ∪ {x}, V' x_1 = Function.updateITE V x d x_1
Tactic:
intro v a1
Proof state after:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (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 =>
                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 ∪ {x}) phi
h2 : ∀ x ∉ binders, V' x = V x
d : D
v : VarName
a1 : v ∉ binders ∪ {x}
⊢ V' v = Function.updateITE V x d v
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.substitution_theorem_aux
Proof state before:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (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 =>
                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 ∪ {x}) phi
h2 : ∀ x ∉ binders, V' x = V x
d : D
v : VarName
a1 : v ∉ binders ∪ {x}
⊢ V' v = Function.updateITE V x d v
Tactic:
simp only [Function.updateITE]
Proof state after:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (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 =>
                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 ∪ {x}) phi
h2 : ∀ x ∉ binders, V' x = V x
d : D
v : VarName
a1 : v ∉ binders ∪ {x}
⊢ V' v = if v = x then d else V v
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.substitution_theorem_aux
Proof state before:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (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 =>
                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 ∪ {x}) phi
h2 : ∀ x ∉ binders, V' x = V x
d : D
v : VarName
a1 : v ∉ binders ∪ {x}
⊢ V' v = if v = x then d else V v
Tactic:
simp at a1
Proof state after:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (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 =>
                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 ∪ {x}) phi
h2 : ∀ x ∉ binders, V' x = V x
d : D
v : VarName
a1 : v ∉ binders ∧ ¬v = x
⊢ V' v = if v = x then d else V v
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.substitution_theorem_aux
Proof state before:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (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 =>
                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 ∪ {x}) phi
h2 : ∀ x ∉ binders, V' x = V x
d : D
v : VarName
a1 : v ∉ binders ∧ ¬v = x
⊢ V' v = if v = x then d else V v
Tactic:
push_neg at a1
Proof state after:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (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 =>
                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 ∪ {x}) phi
h2 : ∀ x ∉ binders, V' x = V x
d : D
v : VarName
a1 : v ∉ binders ∧ v ≠ x
⊢ V' v = if v = x then d else V v
Theorem: FOL.NV.Sub.Pred.All.Rec.Option.substitution_theorem_aux
Proof state before:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (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 =>
                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 ∪ {x}) phi
h2 : ∀ x ∉ binders, V' x = V x
d : D
v : VarName
a1 : v ∉ binders ∧ v ≠ x
⊢ V' v = if v = x then d else V v
Tactic:
cases a1
Proof state after:
case h.intro
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (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 =>
                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 ∪ {x}) phi
h2 : ∀ x ∉ binders, V' x = V x
d : D
v : VarName
left✝ : v ∉ binders
right✝ : v ≠ x
⊢ V' v = if v = x then d else V v
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 : 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 =>
                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 ∪ {x}) phi
h2 : ∀ x ∉ binders, V' x = V x
d : D
v : VarName
a1_left : v ∉ binders
a1_right : v ≠ x
⊢ V' v = if v = x then d else V v
Tactic:
case h.intro a1_left a1_right =>
  simp only [if_neg a1_right]
  exact h2 v a1_left
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 : 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 =>
                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 ∪ {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 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 }
        (Function.updateITE V x d) E phi) ↔
    ∀ (d : D), Holds D I (Function.updateITE V x d) E (replace c τ phi)
Tactic:
apply forall_congr'
Proof state after:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (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 =>
                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 ∪ {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 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 }
        (Function.updateITE V x a) E phi ↔
      Holds D I (Function.updateITE V x a) E (replace c τ phi)
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 : 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 =>
                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 ∪ {x}) phi
h2 : ∀ x ∉ binders, V' x = V x
⊢ (∃ d,
      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 }
        (Function.updateITE V x d) E phi) ↔
    ∃ d, Holds D I (Function.updateITE V x d) E (replace c τ phi)
Tactic:
apply exists_congr
Proof state after:
case h
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (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 =>
                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 ∪ {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 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 }
        (Function.updateITE V x a) E phi ↔
      Holds D I (Function.updateITE V x a) E (replace c τ phi)