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
⊢ (∃ d,
      Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun X ds =>
            if h : (τ X ds.length).isSome = true then
              if ds.length = ((τ X ds.length).get ⋯).1.length then
                Holds D I (Function.updateListITE V'' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
              else I.pred_var_ X ds
            else I.pred_var_ X ds }
        (Function.updateITE V' x d) E phi) ↔
    ∃ d,
      Holds D I
        (Function.updateITE V
          (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)
          d)
        E
        (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:
apply exists_congr
Proof state after:
case h
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
x : VarName
phi : Formula
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
⊢ ∀ (a : D),
    Holds D
        { nonempty := ⋯, pred_const_ := I.pred_const_,
          pred_var_ := fun X ds =>
            if h : (τ X ds.length).isSome = true then
              if ds.length = ((τ X ds.length).get ⋯).1.length then
                Holds D I (Function.updateListITE V'' ((τ X ds.length).get ⋯).1 ds) E ((τ X ds.length).get ⋯).2
              else I.pred_var_ X ds
            else I.pred_var_ X ds }
        (Function.updateITE V' x a) E phi ↔
      Holds D I
        (Function.updateITE V
          (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)
          a)
        E
        (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)