Theorem: FOL.NV.Sub.Pred.All.Rec.Option.Fresh.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V V' V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
σ : VarName → VarName
F : Formula
h1 : ∀ (x : VarName), isFreeIn x F → V' x = V (σ x)
h2 : ∀ x ∈ F.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E F ↔ Holds D I V E (subAux c τ σ F)
Tactic:
induction F generalizing V V' σ
Proof state after:
case pred_const_
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
a✝¹ : PredName
a✝ : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x (pred_const_ a✝¹ a✝) → V' x = V (σ x)
h2 : ∀ x ∈ (pred_const_ a✝¹ a✝).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E (pred_const_ a✝¹ a✝) ↔ Holds D I V E (subAux c τ σ (pred_const_ a✝¹ a✝))

case pred_var_
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
a✝¹ : PredName
a✝ : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x (pred_var_ a✝¹ a✝) → V' x = V (σ x)
h2 : ∀ x ∈ (pred_var_ a✝¹ a✝).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E (pred_var_ a✝¹ a✝) ↔ Holds D I V E (subAux c τ σ (pred_var_ a✝¹ a✝))

case eq_
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
a✝¹ a✝ : VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x (eq_ a✝¹ a✝) → V' x = V (σ x)
h2 : ∀ x ∈ (eq_ a✝¹ a✝).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E (eq_ a✝¹ a✝) ↔ Holds D I V E (subAux c τ σ (eq_ a✝¹ a✝))

case true_
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x true_ → V' x = V (σ x)
h2 : ∀ x ∈ true_.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E true_ ↔ Holds D I V E (subAux c τ σ true_)

case false_
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x false_ → V' x = V (σ x)
h2 : ∀ x ∈ false_.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E false_ ↔ Holds D I V E (subAux c τ σ false_)

case not_
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
a✝ : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x a✝ → V' x = V (σ x)) →
      (∀ x ∈ a✝.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E a✝ ↔ Holds D I V E (subAux c τ σ a✝))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x a✝.not_ → V' x = V (σ x)
h2 : ∀ x ∈ a✝.not_.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E a✝.not_ ↔ Holds D I V E (subAux c τ σ a✝.not_)

case imp_
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x a✝¹ → V' x = V (σ x)) →
      (∀ x ∈ a✝¹.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E a✝¹ ↔ Holds D I V E (subAux c τ σ a✝¹))
a_ih✝ :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x a✝ → V' x = V (σ x)) →
      (∀ x ∈ a✝.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E a✝ ↔ Holds D I V E (subAux c τ σ a✝))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x (a✝¹.imp_ a✝) → V' x = V (σ x)
h2 : ∀ x ∈ (a✝¹.imp_ a✝).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E (a✝¹.imp_ a✝) ↔ Holds D I V E (subAux c τ σ (a✝¹.imp_ a✝))

case and_
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x a✝¹ → V' x = V (σ x)) →
      (∀ x ∈ a✝¹.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E a✝¹ ↔ Holds D I V E (subAux c τ σ a✝¹))
a_ih✝ :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x a✝ → V' x = V (σ x)) →
      (∀ x ∈ a✝.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E a✝ ↔ Holds D I V E (subAux c τ σ a✝))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x (a✝¹.and_ a✝) → V' x = V (σ x)
h2 : ∀ x ∈ (a✝¹.and_ a✝).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E (a✝¹.and_ a✝) ↔ Holds D I V E (subAux c τ σ (a✝¹.and_ a✝))

case or_
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x a✝¹ → V' x = V (σ x)) →
      (∀ x ∈ a✝¹.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E a✝¹ ↔ Holds D I V E (subAux c τ σ a✝¹))
a_ih✝ :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x a✝ → V' x = V (σ x)) →
      (∀ x ∈ a✝.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E a✝ ↔ Holds D I V E (subAux c τ σ a✝))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x (a✝¹.or_ a✝) → V' x = V (σ x)
h2 : ∀ x ∈ (a✝¹.or_ a✝).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E (a✝¹.or_ a✝) ↔ Holds D I V E (subAux c τ σ (a✝¹.or_ a✝))

case iff_
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x a✝¹ → V' x = V (σ x)) →
      (∀ x ∈ a✝¹.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E a✝¹ ↔ Holds D I V E (subAux c τ σ a✝¹))
a_ih✝ :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x a✝ → V' x = V (σ x)) →
      (∀ x ∈ a✝.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E a✝ ↔ Holds D I V E (subAux c τ σ a✝))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x (a✝¹.iff_ a✝) → V' x = V (σ x)
h2 : ∀ x ∈ (a✝¹.iff_ a✝).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E (a✝¹.iff_ a✝) ↔ Holds D I V E (subAux c τ σ (a✝¹.iff_ a✝))

case forall_
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x a✝ → V' x = V (σ x)) →
      (∀ x ∈ a✝.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E a✝ ↔ Holds D I V E (subAux c τ σ a✝))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x (forall_ a✝¹ a✝) → V' x = V (σ x)
h2 : ∀ x ∈ (forall_ a✝¹ a✝).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E (forall_ a✝¹ a✝) ↔ Holds D I V E (subAux c τ σ (forall_ a✝¹ a✝))

case exists_
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (V V' : VarAssignment D) (σ : VarName → VarName),
    (∀ (x : VarName), isFreeIn x a✝ → V' x = V (σ x)) →
      (∀ x ∈ a✝.predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x) →
        (Holds D (I' D I V'' E τ) V' E a✝ ↔ Holds D I V E (subAux c τ σ a✝))
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x (exists_ a✝¹ a✝) → V' x = V (σ x)
h2 : ∀ x ∈ (exists_ a✝¹ a✝).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E (exists_ a✝¹ a✝) ↔ Holds D I V E (subAux c τ σ (exists_ a✝¹ a✝))

case def_
D : Type
I : Interpretation D
V'' : VarAssignment D
E : Env
c : Char
τ : PredName → ℕ → Option (List VarName × Formula)
a✝¹ : DefName
a✝ : List VarName
V V' : VarAssignment D
σ : VarName → VarName
h1 : ∀ (x : VarName), isFreeIn x (def_ a✝¹ a✝) → V' x = V (σ x)
h2 : ∀ x ∈ (def_ a✝¹ a✝).predVarSet.biUnion (predVarFreeVarSet τ), V'' x = V x
⊢ Holds D (I' D I V'' E τ) V' E (def_ a✝¹ a✝) ↔ Holds D I V E (subAux c τ σ (def_ a✝¹ a✝))