Theorem: FOL.NV.Sub.Pred.All.Rec.substitution_theorem_aux (FOL/NV/Sub/Pred/All/Rec/Sub.lean)

State before:
D : Type
I : Interpretation D
V V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
binders : Finset VarName
F : Formula
h1 : admitsAux τ binders F
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 F ↔
    Holds D I V E (replace τ F)
Tactic:
induction F generalizing binders V
State after:
case pred_const_
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
a✝¹ : PredName
a✝ : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (pred_const_ a✝¹ a✝)
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 (pred_const_ a✝¹ a✝) ↔
    Holds D I V E (replace τ (pred_const_ a✝¹ a✝))

case pred_var_
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
a✝¹ : PredName
a✝ : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (pred_var_ a✝¹ a✝)
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 (pred_var_ a✝¹ a✝) ↔
    Holds D I V E (replace τ (pred_var_ a✝¹ a✝))

case eq_
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
a✝¹ a✝ : VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (eq_ a✝¹ a✝)
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_ a✝¹ a✝) ↔
    Holds D I V E (replace τ (eq_ a✝¹ a✝))

case true_
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders true_
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 true_ ↔
    Holds D I V E (replace τ true_)

case false_
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_)

case not_
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders a✝ →
      (∀ 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 a✝ ↔
          Holds D I V E (replace τ a✝))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders a✝.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 a✝.not_ ↔
    Holds D I V E (replace τ a✝.not_)

case imp_
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders a✝¹ →
      (∀ 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 a✝¹ ↔
          Holds D I V E (replace τ a✝¹))
a_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders a✝ →
      (∀ 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 a✝ ↔
          Holds D I V E (replace τ a✝))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (a✝¹.imp_ a✝)
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 (a✝¹.imp_ a✝) ↔
    Holds D I V E (replace τ (a✝¹.imp_ a✝))

case and_
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders a✝¹ →
      (∀ 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 a✝¹ ↔
          Holds D I V E (replace τ a✝¹))
a_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders a✝ →
      (∀ 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 a✝ ↔
          Holds D I V E (replace τ a✝))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (a✝¹.and_ a✝)
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 (a✝¹.and_ a✝) ↔
    Holds D I V E (replace τ (a✝¹.and_ a✝))

case or_
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders a✝¹ →
      (∀ 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 a✝¹ ↔
          Holds D I V E (replace τ a✝¹))
a_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders a✝ →
      (∀ 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 a✝ ↔
          Holds D I V E (replace τ a✝))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (a✝¹.or_ a✝)
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 (a✝¹.or_ a✝) ↔
    Holds D I V E (replace τ (a✝¹.or_ a✝))

case iff_
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders a✝¹ →
      (∀ 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 a✝¹ ↔
          Holds D I V E (replace τ a✝¹))
a_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders a✝ →
      (∀ 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 a✝ ↔
          Holds D I V E (replace τ a✝))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (a✝¹.iff_ a✝)
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 (a✝¹.iff_ a✝) ↔
    Holds D I V E (replace τ (a✝¹.iff_ a✝))

case forall_
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders a✝ →
      (∀ 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 a✝ ↔
          Holds D I V E (replace τ a✝))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (forall_ a✝¹ a✝)
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 (forall_ a✝¹ a✝) ↔
    Holds D I V E (replace τ (forall_ a✝¹ a✝))

case exists_
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (V : VarAssignment D) (binders : Finset VarName),
    admitsAux τ binders a✝ →
      (∀ 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 a✝ ↔
          Holds D I V E (replace τ a✝))
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (exists_ a✝¹ a✝)
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_ a✝¹ a✝) ↔
    Holds D I V E (replace τ (exists_ a✝¹ a✝))

case def_
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
a✝¹ : DefName
a✝ : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ a✝¹ a✝)
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 (def_ a✝¹ a✝) ↔
    Holds D I V E (replace τ (def_ a✝¹ a✝))

State before:
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 : admitsAux τ binders (pred_const_ X xs)
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 (pred_const_ X xs) ↔
    Holds D I V E (replace τ (pred_const_ X xs))
Tactic:
case pred_const_ X xs =>
  simp only [replace]
  simp only [Holds]
State after:
no goals

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:
case eq_ x y =>
  simp only [replace]
  simp only [Holds]
State after:
no goals

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:
case true_ | false_ =>
  simp only [replace]
  simp only [Holds]
State after:
no goals

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:
case not_ phi phi_ih =>
  simp only [admitsAux] at h1
  simp only [replace]
  simp only [Holds]
  congr! 1
  exact phi_ih V binders h1 h2
State after:
no goals

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:
case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  simp only [admitsAux] at h1
  simp only [replace]
  simp only [Holds]
  first | apply forall_congr' | apply exists_congr
  intro d
  apply phi_ih (Function.updateITE V x d) (binders ∪ {x}) h1
  intro v a1
  simp only [Function.updateITE]
  simp at a1
  push_neg at a1
  cases a1
  case h.intro a1_left a1_right =>
    simp only [if_neg a1_right]
    exact h2 v a1_left
State after:
no goals

State before:
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 : admitsAux τ binders (pred_const_ X xs)
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 (pred_const_ X xs) ↔
    Holds D I V E (replace τ (pred_const_ X xs))
Tactic:
simp only [replace]
State after:
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 : admitsAux τ binders (pred_const_ X xs)
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 (pred_const_ X xs) ↔
    Holds D I V E (pred_const_ X xs)

State before:
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 : admitsAux τ binders (pred_const_ X xs)
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 (pred_const_ X xs) ↔
    Holds D I V E (pred_const_ X xs)
Tactic:
simp only [Holds]
State after:
no goals

State before:
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 : admitsAux τ binders (pred_var_ X xs)
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 (pred_var_ X xs) ↔
    Holds D I V E (replace τ (pred_var_ X xs))
Tactic:
simp only [admitsAux] at h1
State after:
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 :
  Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2 ∧
    (∀ x ∈ binders, ¬(isFreeIn x (τ X xs.length).2 ∧ x ∉ (τ X xs.length).1)) ∧ xs.length = (τ X xs.length).1.length
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 (pred_var_ X xs) ↔
    Holds D I V E (replace τ (pred_var_ X xs))

State before:
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 :
  Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2 ∧
    (∀ x ∈ binders, ¬(isFreeIn x (τ X xs.length).2 ∧ x ∉ (τ X xs.length).1)) ∧ xs.length = (τ X xs.length).1.length
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 (pred_var_ X xs) ↔
    Holds D I V E (replace τ (pred_var_ X xs))
Tactic:
simp at h1
State after:
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 :
  Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2 ∧
    (∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1) ∧ xs.length = (τ X xs.length).1.length
⊢ 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 (pred_var_ X xs) ↔
    Holds D I V E (replace τ (pred_var_ X xs))

State before:
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 :
  Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2 ∧
    (∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1) ∧ xs.length = (τ X xs.length).1.length
⊢ 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 (pred_var_ X xs) ↔
    Holds D I V E (replace τ (pred_var_ X xs))
Tactic:
cases h1
State after:
case intro
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
left✝ : Var.All.Rec.admits (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
right✝ : (∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1) ∧ xs.length = (τ X xs.length).1.length
⊢ 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 (pred_var_ X xs) ↔
    Holds D I V E (replace τ (pred_var_ X xs))

State before:
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 : (∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1) ∧ xs.length = (τ X xs.length).1.length
⊢ 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 (pred_var_ X xs) ↔
    Holds D I V E (replace τ (pred_var_ X xs))
Tactic:
cases h1_right
State after:
case intro
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
left✝ : ∀ x ∈ binders, isFreeIn x (τ X xs.length).2 → x ∈ (τ X xs.length).1
right✝ : xs.length = (τ X xs.length).1.length
⊢ 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 (pred_var_ X xs) ↔
    Holds D I V E (replace τ (pred_var_ X xs))

State before:
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
⊢ 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 (pred_var_ X xs) ↔
    Holds D I V E (replace τ (pred_var_ X xs))
Tactic:
obtain s1 :=
Sub.Var.All.Rec.substitution_theorem D I V E (Function.updateListITE id (τ X xs.length).fst xs)
  (τ X xs.length).snd h1_left
State after:
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 (V ∘ Function.updateListITE id (τ X xs.length).1 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)
⊢ 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 (pred_var_ X xs) ↔
    Holds D I V E (replace τ (pred_var_ X xs))

State before:
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 (V ∘ Function.updateListITE id (τ X xs.length).1 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)
⊢ 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 (pred_var_ X xs) ↔
    Holds D I V E (replace τ (pred_var_ X xs))
Tactic:
simp only [Function.updateListITE_comp] at s1
State after:
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 ∘ id) (τ 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)
⊢ 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 (pred_var_ X xs) ↔
    Holds D I V E (replace τ (pred_var_ X xs))

State before:
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 ∘ id) (τ 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)
⊢ 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 (pred_var_ X xs) ↔
    Holds D I V E (replace τ (pred_var_ X xs))
Tactic:
simp at s1
State after:
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)
⊢ 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 (pred_var_ X xs) ↔
    Holds D I V E (replace τ (pred_var_ X xs))

State before:
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)
s2 :
  Holds D I (Function.updateListITE V (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I (Function.updateListITE V' (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2
⊢ 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 (pred_var_ X xs) ↔
    Holds D I V E (replace τ (pred_var_ X xs))
Tactic:
simp only [s2] at s1
State after:
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
s2 :
  Holds D I (Function.updateListITE V (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I (Function.updateListITE V' (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2
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)
⊢ 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 (pred_var_ X xs) ↔
    Holds D I V E (replace τ (pred_var_ X xs))

State before:
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
s2 :
  Holds D I (Function.updateListITE V (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I (Function.updateListITE V' (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2
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)
⊢ 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 (pred_var_ X xs) ↔
    Holds D I V E (replace τ (pred_var_ X xs))
Tactic:
clear s2
State after:
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)
⊢ 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 (pred_var_ X xs) ↔
    Holds D I V E (replace τ (pred_var_ X xs))

State before:
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)
⊢ 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 (pred_var_ X xs) ↔
    Holds D I V E (replace τ (pred_var_ X xs))
Tactic:
simp only [Holds]
State after:
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)
⊢ (if (List.map V xs).length = (τ X (List.map V xs).length).1.length then
      Holds D I (Function.updateListITE V' (τ X (List.map V xs).length).1 (List.map V xs)) E
        (τ X (List.map V xs).length).2
    else I.pred_var_ X (List.map V xs)) ↔
    Holds D I V E (replace τ (pred_var_ X xs))

State before:
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)
⊢ (if (List.map V xs).length = (τ X (List.map V xs).length).1.length then
      Holds D I (Function.updateListITE V' (τ X (List.map V xs).length).1 (List.map V xs)) E
        (τ X (List.map V xs).length).2
    else I.pred_var_ X (List.map V xs)) ↔
    Holds D I V E (replace τ (pred_var_ X xs))
Tactic:
simp only [replace]
State after:
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)
⊢ (if (List.map V xs).length = (τ X (List.map V xs).length).1.length then
      Holds D I (Function.updateListITE V' (τ X (List.map V xs).length).1 (List.map V xs)) E
        (τ X (List.map V xs).length).2
    else I.pred_var_ X (List.map V xs)) ↔
    Holds D I V E
      (if xs.length = (τ X xs.length).1.length then
        Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
      else pred_var_ X xs)

State before:
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)
⊢ (if (List.map V xs).length = (τ X (List.map V xs).length).1.length then
      Holds D I (Function.updateListITE V' (τ X (List.map V xs).length).1 (List.map V xs)) E
        (τ X (List.map V xs).length).2
    else I.pred_var_ X (List.map V xs)) ↔
    Holds D I V E
      (if xs.length = (τ X xs.length).1.length then
        Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
      else pred_var_ X xs)
Tactic:
simp
State after:
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)
⊢ (if xs.length = (τ X xs.length).1.length then
      Holds D I (Function.updateListITE V' (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2
    else I.pred_var_ X (List.map V xs)) ↔
    Holds D I V E
      (if xs.length = (τ X xs.length).1.length then
        Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
      else pred_var_ X xs)

State before:
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)
⊢ (if xs.length = (τ X xs.length).1.length then
      Holds D I (Function.updateListITE V' (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2
    else I.pred_var_ X (List.map V xs)) ↔
    Holds D I V E
      (if xs.length = (τ X xs.length).1.length then
        Var.All.Rec.fastReplaceFree (Function.updateListITE id (τ X xs.length).1 xs) (τ X xs.length).2
      else pred_var_ X xs)
Tactic:
simp only [if_pos h1_right_right]
State after:
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)
⊢ 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)

State before:
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)
⊢ 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)
Tactic:
exact s1
State after:
no goals

State before:
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)
⊢ Holds D I (Function.updateListITE V (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2 ↔
    Holds D I (Function.updateListITE V' (τ X xs.length).1 (List.map V xs)) E (τ X xs.length).2
Tactic:
apply Holds_coincide_Var
State after:
case 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
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),
    isFreeIn v (τ X xs.length).2 →
      Function.updateListITE V (τ X xs.length).1 (List.map V xs) v =
        Function.updateListITE V' (τ X xs.length).1 (List.map V xs) v

State before:
case 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
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),
    isFreeIn v (τ X xs.length).2 →
      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:
intro v a1
State after:
case 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
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
⊢ Function.updateListITE V (τ X xs.length).1 (List.map V xs) v =
    Function.updateListITE V' (τ X xs.length).1 (List.map V xs) v

State before:
case 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
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
⊢ 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 c1 : v ∈ (τ X xs.length).fst
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
⊢ 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
⊢ Function.updateListITE V (τ X xs.length).1 (List.map V xs) v =
    Function.updateListITE V' (τ X xs.length).1 (List.map V xs) v

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
⊢ 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_eq_len V V' v (τ X xs.length).fst (List.map V xs) c1
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
⊢ (τ X xs.length).1.length = (List.map V xs).length

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 = (List.map V xs).length
Tactic:
simp
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
⊢ (τ X xs.length).1.length = xs.length

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
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

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
State after:
no goals

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
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

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
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

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
State after:
no goals

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
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

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'
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

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
State after:
no goals

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]
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)

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]
State after:
no goals

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]
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_

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]
State after:
no goals

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
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_)

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]
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_

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]
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)

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
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)

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
State after:
no goals

State before:
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
h1 : admitsAux τ binders (phi.iff_ psi)
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.iff_ psi) ↔
    Holds D I V E (replace τ (phi.iff_ psi))
Tactic:
simp only [admitsAux] at h1
State after:
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
h1 : admitsAux τ binders phi ∧ admitsAux τ binders psi
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.iff_ psi) ↔
    Holds D I V E (replace τ (phi.iff_ psi))

State before:
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
h1 : admitsAux τ binders phi ∧ admitsAux τ binders psi
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.iff_ psi) ↔
    Holds D I V E (replace τ (phi.iff_ psi))
Tactic:
simp only [replace]
State after:
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
h1 : admitsAux τ binders phi ∧ admitsAux τ binders psi
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.iff_ psi) ↔
    Holds D I V E ((replace τ phi).iff_ (replace τ psi))

State before:
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
h1 : admitsAux τ binders phi ∧ admitsAux τ binders psi
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.iff_ psi) ↔
    Holds D I V E ((replace τ phi).iff_ (replace τ psi))
Tactic:
simp only [Holds]
State after:
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
h1 : admitsAux τ binders phi ∧ admitsAux τ binders psi
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
        { 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 τ phi) ↔ Holds D I V E (replace τ psi))

State before:
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
h1 : admitsAux τ binders phi ∧ admitsAux τ binders psi
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
        { 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 τ phi) ↔ Holds D I V E (replace τ psi))
Tactic:
cases h1
State after:
case intro
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
left✝ : admitsAux τ binders phi
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
        { 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 τ phi) ↔ Holds D I V E (replace τ psi))

State before:
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
        { 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 τ phi) ↔ Holds D I V E (replace τ psi))
Tactic:
congr! 1
State after:
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)

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)

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
State after:
no goals

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
State after:
no goals

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
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))

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]
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))

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]
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)

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
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)

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
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)

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
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

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
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

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
v : VarName
a1 : v ∉ binders ∪ {x}
⊢ Function.updateITE V x d v = V' v
Tactic:
simp only [Function.updateITE]
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}
⊢ (if v = x then d else V v) = V' v

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
v : VarName
a1 : v ∉ binders ∪ {x}
⊢ (if v = x then d else V v) = V' v
Tactic:
simp at a1
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 ∧ ¬v = x
⊢ (if v = x then d else V v) = V' v

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
v : VarName
a1 : v ∉ binders ∧ ¬v = x
⊢ (if v = x then d else V v) = V' v
Tactic:
push_neg at a1
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 ∧ v ≠ x
⊢ (if v = x then d else V v) = V' v

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
v : VarName
a1 : v ∉ binders ∧ v ≠ x
⊢ (if v = x then d else V v) = V' v
Tactic:
cases a1
State after:
case h.intro
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
left✝ : v ∉ binders
right✝ : v ≠ x
⊢ (if v = x then d else V v) = V' v

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 : D
v : VarName
a1_left : v ∉ binders
a1_right : v ≠ x
⊢ (if v = x then d else V v) = V' v
Tactic:
case h.intro a1_left a1_right =>
  simp only [if_neg a1_right]
  exact h2 v a1_left
State after:
no goals

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 : 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 : D), Holds D I (Function.updateITE V x d) E (replace τ phi)
Tactic:
apply forall_congr'
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)

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:
apply exists_congr
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)

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 : D
v : VarName
a1_left : v ∉ binders
a1_right : v ≠ x
⊢ (if v = x then d else V v) = V' v
Tactic:
simp only [if_neg a1_right]
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 : D
v : VarName
a1_left : v ∉ binders
a1_right : v ≠ x
⊢ V v = V' v

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 : D
v : VarName
a1_left : v ∉ binders
a1_right : v ≠ x
⊢ V v = V' v
Tactic:
exact h2 v a1_left
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
E : Env
τ : PredName → ℕ → List VarName × Formula
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
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 (def_ X xs) ↔
    Holds D I V E (replace τ (def_ X xs))
Tactic:
cases E
State after:
case nil
D : Type
I : Interpretation D
V' : VarAssignment D
τ : PredName → ℕ → List VarName × Formula
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
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) [] (τ X ds.length).2
          else I.pred_var_ X ds }
      V [] (def_ X xs) ↔
    Holds D I V [] (replace τ (def_ X xs))

case cons
D : Type
I : Interpretation D
V' : VarAssignment D
τ : PredName → ℕ → List VarName × Formula
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
head✝ : Definition
tail✝ : List Definition
⊢ 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) (head✝ :: tail✝) (τ X ds.length).2
          else I.pred_var_ X ds }
      V (head✝ :: tail✝) (def_ X xs) ↔
    Holds D I V (head✝ :: tail✝) (replace τ (def_ X xs))

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
τ : PredName → ℕ → List VarName × Formula
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
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) [] (τ X ds.length).2
          else I.pred_var_ X ds }
      V [] (def_ X xs) ↔
    Holds D I V [] (replace τ (def_ X xs))
Tactic:
case nil =>
  simp only [replace]
  simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
τ : PredName → ℕ → List VarName × Formula
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
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) [] (τ X ds.length).2
          else I.pred_var_ X ds }
      V [] (def_ X xs) ↔
    Holds D I V [] (replace τ (def_ X xs))
Tactic:
simp only [replace]
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
τ : PredName → ℕ → List VarName × Formula
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
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) [] (τ X ds.length).2
          else I.pred_var_ X ds }
      V [] (def_ X xs) ↔
    Holds D I V [] (def_ X xs)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
τ : PredName → ℕ → List VarName × Formula
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
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) [] (τ X ds.length).2
          else I.pred_var_ X ds }
      V [] (def_ X xs) ↔
    Holds D I V [] (def_ X xs)
Tactic:
simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
τ : PredName → ℕ → List VarName × Formula
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
hd : Definition
tl : List Definition
⊢ 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) (hd :: tl) (τ X ds.length).2
          else I.pred_var_ X ds }
      V (hd :: tl) (def_ X xs) ↔
    Holds D I V (hd :: tl) (replace τ (def_ X xs))
Tactic:
simp only [replace]
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
τ : PredName → ℕ → List VarName × Formula
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
hd : Definition
tl : List Definition
⊢ 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) (hd :: tl) (τ X ds.length).2
          else I.pred_var_ X ds }
      V (hd :: tl) (def_ X xs) ↔
    Holds D I V (hd :: tl) (def_ X xs)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
τ : PredName → ℕ → List VarName × Formula
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
hd : Definition
tl : List Definition
⊢ 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) (hd :: tl) (τ X ds.length).2
          else I.pred_var_ X ds }
      V (hd :: tl) (def_ X xs) ↔
    Holds D I V (hd :: tl) (def_ X xs)
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
V' : VarAssignment D
τ : PredName → ℕ → List VarName × Formula
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
hd : Definition
tl : List Definition
⊢ (if X = hd.name ∧ xs.length = hd.args.length then
      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) (hd :: tl) (τ X ds.length).2
            else I.pred_var_ X ds }
        (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
    else
      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) (hd :: tl) (τ X ds.length).2
            else I.pred_var_ X ds }
        V tl (def_ X xs)) ↔
    if X = hd.name ∧ xs.length = hd.args.length then
      Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
    else Holds D I V tl (def_ X xs)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
τ : PredName → ℕ → List VarName × Formula
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
hd : Definition
tl : List Definition
⊢ (if X = hd.name ∧ xs.length = hd.args.length then
      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) (hd :: tl) (τ X ds.length).2
            else I.pred_var_ X ds }
        (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
    else
      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) (hd :: tl) (τ X ds.length).2
            else I.pred_var_ X ds }
        V tl (def_ X xs)) ↔
    if X = hd.name ∧ xs.length = hd.args.length then
      Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
    else Holds D I V tl (def_ X xs)
Tactic:
split_ifs
State after:
case pos
D : Type
I : Interpretation D
V' : VarAssignment D
τ : PredName → ℕ → List VarName × Formula
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
hd : Definition
tl : List Definition
h✝ : X = hd.name ∧ xs.length = hd.args.length
⊢ 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) (hd :: tl) (τ X ds.length).2
          else I.pred_var_ X ds }
      (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔
    Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q

case neg
D : Type
I : Interpretation D
V' : VarAssignment D
τ : PredName → ℕ → List VarName × Formula
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
hd : Definition
tl : List Definition
h✝ : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ 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) (hd :: tl) (τ X ds.length).2
          else I.pred_var_ X ds }
      V tl (def_ X xs) ↔
    Holds D I V tl (def_ X xs)

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
τ : PredName → ℕ → List VarName × Formula
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
hd : Definition
tl : List Definition
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ 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) (hd :: tl) (τ X ds.length).2
          else I.pred_var_ X ds }
      (Function.updateListITE V hd.args (List.map V xs)) tl hd.q ↔
    Holds D I (Function.updateListITE V hd.args (List.map V xs)) tl hd.q
Tactic:
apply Holds_coincide_PredVar
State after:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
τ : PredName → ℕ → List VarName × Formula
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
hd : Definition
tl : List Definition
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ { 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) (hd :: tl) (τ X ds.length).2
          else I.pred_var_ X ds }.pred_const_ =
    I.pred_const_

case h2
D : Type
I : Interpretation D
V' : VarAssignment D
τ : PredName → ℕ → List VarName × Formula
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
hd : Definition
tl : List Definition
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length hd.q →
      ({ 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) (hd :: tl) (τ X ds.length).2
                else I.pred_var_ X ds }.pred_var_
          P ds ↔
        I.pred_var_ P ds)

State before:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
τ : PredName → ℕ → List VarName × Formula
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
hd : Definition
tl : List Definition
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ { 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) (hd :: tl) (τ X ds.length).2
          else I.pred_var_ X ds }.pred_const_ =
    I.pred_const_
Tactic:
simp
State after:
no goals

State before:
case h2
D : Type
I : Interpretation D
V' : VarAssignment D
τ : PredName → ℕ → List VarName × Formula
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
hd : Definition
tl : List Definition
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length hd.q →
      ({ 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) (hd :: tl) (τ X ds.length).2
                else I.pred_var_ X ds }.pred_var_
          P ds ↔
        I.pred_var_ P ds)
Tactic:
simp only [predVarOccursIn_iff_mem_predVarSet]
State after:
case h2
D : Type
I : Interpretation D
V' : VarAssignment D
τ : PredName → ℕ → List VarName × Formula
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
hd : Definition
tl : List Definition
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ ∀ (P : PredName) (ds : List D),
    (P, ds.length) ∈ hd.q.predVarSet →
      ((if ds.length = (τ P ds.length).1.length then
          Holds D I (Function.updateListITE V' (τ P ds.length).1 ds) (hd :: tl) (τ P ds.length).2
        else I.pred_var_ P ds) ↔
        I.pred_var_ P ds)

State before:
case h2
D : Type
I : Interpretation D
V' : VarAssignment D
τ : PredName → ℕ → List VarName × Formula
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
hd : Definition
tl : List Definition
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ ∀ (P : PredName) (ds : List D),
    (P, ds.length) ∈ hd.q.predVarSet →
      ((if ds.length = (τ P ds.length).1.length then
          Holds D I (Function.updateListITE V' (τ P ds.length).1 ds) (hd :: tl) (τ P ds.length).2
        else I.pred_var_ P ds) ↔
        I.pred_var_ P ds)
Tactic:
simp only [hd.h2]
State after:
case h2
D : Type
I : Interpretation D
V' : VarAssignment D
τ : PredName → ℕ → List VarName × Formula
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
hd : Definition
tl : List Definition
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ ∀ (P : PredName) (ds : List D),
    (P, ds.length) ∈ ∅ →
      ((if ds.length = (τ P ds.length).1.length then
          Holds D I (Function.updateListITE V' (τ P ds.length).1 ds) (hd :: tl) (τ P ds.length).2
        else I.pred_var_ P ds) ↔
        I.pred_var_ P ds)

State before:
case h2
D : Type
I : Interpretation D
V' : VarAssignment D
τ : PredName → ℕ → List VarName × Formula
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
hd : Definition
tl : List Definition
c1 : X = hd.name ∧ xs.length = hd.args.length
⊢ ∀ (P : PredName) (ds : List D),
    (P, ds.length) ∈ ∅ →
      ((if ds.length = (τ P ds.length).1.length then
          Holds D I (Function.updateListITE V' (τ P ds.length).1 ds) (hd :: tl) (τ P ds.length).2
        else I.pred_var_ P ds) ↔
        I.pred_var_ P ds)
Tactic:
simp
State after:
no goals

State before:
D : Type
I : Interpretation D
V' : VarAssignment D
τ : PredName → ℕ → List VarName × Formula
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
hd : Definition
tl : List Definition
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ 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) (hd :: tl) (τ X ds.length).2
          else I.pred_var_ X ds }
      V tl (def_ X xs) ↔
    Holds D I V tl (def_ X xs)
Tactic:
apply Holds_coincide_PredVar
State after:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
τ : PredName → ℕ → List VarName × Formula
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
hd : Definition
tl : List Definition
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ { 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) (hd :: tl) (τ X ds.length).2
          else I.pred_var_ X ds }.pred_const_ =
    I.pred_const_

case h2
D : Type
I : Interpretation D
V' : VarAssignment D
τ : PredName → ℕ → List VarName × Formula
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
hd : Definition
tl : List Definition
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length (def_ X xs) →
      ({ 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) (hd :: tl) (τ X ds.length).2
                else I.pred_var_ X ds }.pred_var_
          P ds ↔
        I.pred_var_ P ds)

State before:
case h1
D : Type
I : Interpretation D
V' : VarAssignment D
τ : PredName → ℕ → List VarName × Formula
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
hd : Definition
tl : List Definition
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ { 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) (hd :: tl) (τ X ds.length).2
          else I.pred_var_ X ds }.pred_const_ =
    I.pred_const_
Tactic:
simp
State after:
no goals

State before:
case h2
D : Type
I : Interpretation D
V' : VarAssignment D
τ : PredName → ℕ → List VarName × Formula
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
hd : Definition
tl : List Definition
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ ∀ (P : PredName) (ds : List D),
    predVarOccursIn P ds.length (def_ X xs) →
      ({ 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) (hd :: tl) (τ X ds.length).2
                else I.pred_var_ X ds }.pred_var_
          P ds ↔
        I.pred_var_ P ds)
Tactic:
simp only [predVarOccursIn]
State after:
case h2
D : Type
I : Interpretation D
V' : VarAssignment D
τ : PredName → ℕ → List VarName × Formula
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
hd : Definition
tl : List Definition
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ ∀ (P : PredName) (ds : List D),
    False →
      ((if ds.length = (τ P ds.length).1.length then
          Holds D I (Function.updateListITE V' (τ P ds.length).1 ds) (hd :: tl) (τ P ds.length).2
        else I.pred_var_ P ds) ↔
        I.pred_var_ P ds)

State before:
case h2
D : Type
I : Interpretation D
V' : VarAssignment D
τ : PredName → ℕ → List VarName × Formula
X : DefName
xs : List VarName
V : VarAssignment D
binders : Finset VarName
h1 : admitsAux τ binders (def_ X xs)
h2 : ∀ x ∉ binders, V x = V' x
hd : Definition
tl : List Definition
c1 : ¬(X = hd.name ∧ xs.length = hd.args.length)
⊢ ∀ (P : PredName) (ds : List D),
    False →
      ((if ds.length = (τ P ds.length).1.length then
          Holds D I (Function.updateListITE V' (τ P ds.length).1 ds) (hd :: tl) (τ P ds.length).2
        else I.pred_var_ P ds) ↔
        I.pred_var_ P ds)
Tactic:
simp
State after:
no goals