Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), ¬x_1 = x ∧ isFreeIn x_1 phi → V' x_1 = V (σ x_1)
h2 : ∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D
      (Interpretation.usingPred D I fun X ds =>
        if h : (τ X ds.length).isSome = true then
          if ds.length = ((τ X ds.length).get ⋯).1.length then
            Holds D I (Function.updateListITE V'' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
          else I.pred_var_ X ds
        else I.pred_var_ X ds)
      V' E (exists_ x phi) ↔
    Holds D I V E
      (exists_
        (if
            x ∈
              Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪ phi.predVarSet.biUnion (predVarFreeVarSet τ) then
          fresh x c
            (Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪ phi.predVarSet.biUnion (predVarFreeVarSet τ))
        else x)
        (subAux c τ
          (Function.updateITE σ x
            (if
                x ∈
                  Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪
                    phi.predVarSet.biUnion (predVarFreeVarSet τ) then
              fresh x c
                (Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪ phi.predVarSet.biUnion (predVarFreeVarSet τ))
            else x))
          phi))
Tactic:
simp only [Interpretation.usingPred]
Proof state after:
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
ih :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x phi → V' x = V (σ x)) →
      (∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E phi ↔ Holds D I V E (subAux c τ σ phi))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x_1 : VarName), ¬x_1 = x ∧ isFreeIn x_1 phi → V' x_1 = V (σ x_1)
h2 : ∀ x ∈ phi.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D
      { nonempty := ⋯, pred_const_ := I.pred_const_,
        pred_var_ := fun X ds =>
          if h : (τ X ds.length).isSome = true then
            if ds.length = ((τ X ds.length).get ⋯).1.length then
              Holds D I (Function.updateListITE V'' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
            else I.pred_var_ X ds
          else I.pred_var_ X ds }
      V' E (exists_ x phi) ↔
    Holds D I V E
      (exists_
        (if
            x ∈
              Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪ phi.predVarSet.biUnion (predVarFreeVarSet τ) then
          fresh x c
            (Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪ phi.predVarSet.biUnion (predVarFreeVarSet τ))
        else x)
        (subAux c τ
          (Function.updateITE σ x
            (if
                x ∈
                  Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪
                    phi.predVarSet.biUnion (predVarFreeVarSet τ) then
              fresh x c
                (Finset.image (Function.updateITE σ x x) phi.freeVarSet ∪ phi.predVarSet.biUnion (predVarFreeVarSet τ))
            else x))
          phi))