Theorem: FOL.NV.Sub.Var.All.Ind.substitution_theorem_aux
Proof state before:
D : Type
I : Interpretation D
V V' : VarAssignment D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
h1 : IsSubAux σ binders F F'
h2 : ∀ v ∈ binders, V v = V' (σ v)
h3 : ∀ (v : VarName), σ v ∉ binders → V v = V' (σ v)
h4 : ∀ v ∈ binders, v = σ v
⊢ Holds D I V E F ↔ Holds D I V' E F'
Tactic:
induction h1 generalizing V V'
Proof state after:
case pred_const_
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ✝ : VarName → VarName
binders✝ : Finset VarName
X✝ : PredName
xs✝ : List VarName
a✝ : ∀ v ∈ xs✝, v ∉ binders✝ → σ✝ v ∉ binders✝
V V' : VarAssignment D
h2 : ∀ v ∈ binders✝, V v = V' (σ✝ v)
h3 : ∀ (v : VarName), σ✝ v ∉ binders✝ → V v = V' (σ✝ v)
h4 : ∀ v ∈ binders✝, v = σ✝ v
⊢ Holds D I V E (pred_const_ X✝ xs✝) ↔ Holds D I V' E (pred_const_ X✝ (List.map σ✝ xs✝))

case pred_var_
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ✝ : VarName → VarName
binders✝ : Finset VarName
X✝ : PredName
xs✝ : List VarName
a✝ : ∀ v ∈ xs✝, v ∉ binders✝ → σ✝ v ∉ binders✝
V V' : VarAssignment D
h2 : ∀ v ∈ binders✝, V v = V' (σ✝ v)
h3 : ∀ (v : VarName), σ✝ v ∉ binders✝ → V v = V' (σ✝ v)
h4 : ∀ v ∈ binders✝, v = σ✝ v
⊢ Holds D I V E (pred_var_ X✝ xs✝) ↔ Holds D I V' E (pred_var_ X✝ (List.map σ✝ xs✝))

case eq_
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ✝ : VarName → VarName
binders✝ : Finset VarName
x✝ y✝ : VarName
a✝ : ∀ (v : VarName), v = x✝ ∨ v = y✝ → v ∉ binders✝ → σ✝ v ∉ binders✝
V V' : VarAssignment D
h2 : ∀ v ∈ binders✝, V v = V' (σ✝ v)
h3 : ∀ (v : VarName), σ✝ v ∉ binders✝ → V v = V' (σ✝ v)
h4 : ∀ v ∈ binders✝, v = σ✝ v
⊢ Holds D I V E (eq_ x✝ y✝) ↔ Holds D I V' E (eq_ (σ✝ x✝) (σ✝ y✝))

case true_
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ✝ : VarName → VarName
binders✝ : Finset VarName
V V' : VarAssignment D
h2 : ∀ v ∈ binders✝, V v = V' (σ✝ v)
h3 : ∀ (v : VarName), σ✝ v ∉ binders✝ → V v = V' (σ✝ v)
h4 : ∀ v ∈ binders✝, v = σ✝ v
⊢ Holds D I V E true_ ↔ Holds D I V' E true_

case false_
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ✝ : VarName → VarName
binders✝ : Finset VarName
V V' : VarAssignment D
h2 : ∀ v ∈ binders✝, V v = V' (σ✝ v)
h3 : ∀ (v : VarName), σ✝ v ∉ binders✝ → V v = V' (σ✝ v)
h4 : ∀ v ∈ binders✝, v = σ✝ v
⊢ Holds D I V E false_ ↔ Holds D I V' E false_

case not_
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ✝ : VarName → VarName
binders✝ : Finset VarName
phi✝ phi'✝ : Formula
a✝ : IsSubAux σ✝ binders✝ phi✝ phi'✝
a_ih✝ :
  ∀ (V V' : VarAssignment D),
    (∀ v ∈ binders✝, V v = V' (σ✝ v)) →
      (∀ (v : VarName), σ✝ v ∉ binders✝ → V v = V' (σ✝ v)) →
        (∀ v ∈ binders✝, v = σ✝ v) → (Holds D I V E phi✝ ↔ Holds D I V' E phi'✝)
V V' : VarAssignment D
h2 : ∀ v ∈ binders✝, V v = V' (σ✝ v)
h3 : ∀ (v : VarName), σ✝ v ∉ binders✝ → V v = V' (σ✝ v)
h4 : ∀ v ∈ binders✝, v = σ✝ v
⊢ Holds D I V E phi✝.not_ ↔ Holds D I V' E phi'✝.not_

case imp_
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ✝ : VarName → VarName
binders✝ : Finset VarName
phi✝ psi✝ phi'✝ psi'✝ : Formula
a✝¹ : IsSubAux σ✝ binders✝ phi✝ phi'✝
a✝ : IsSubAux σ✝ binders✝ psi✝ psi'✝
a_ih✝¹ :
  ∀ (V V' : VarAssignment D),
    (∀ v ∈ binders✝, V v = V' (σ✝ v)) →
      (∀ (v : VarName), σ✝ v ∉ binders✝ → V v = V' (σ✝ v)) →
        (∀ v ∈ binders✝, v = σ✝ v) → (Holds D I V E phi✝ ↔ Holds D I V' E phi'✝)
a_ih✝ :
  ∀ (V V' : VarAssignment D),
    (∀ v ∈ binders✝, V v = V' (σ✝ v)) →
      (∀ (v : VarName), σ✝ v ∉ binders✝ → V v = V' (σ✝ v)) →
        (∀ v ∈ binders✝, v = σ✝ v) → (Holds D I V E psi✝ ↔ Holds D I V' E psi'✝)
V V' : VarAssignment D
h2 : ∀ v ∈ binders✝, V v = V' (σ✝ v)
h3 : ∀ (v : VarName), σ✝ v ∉ binders✝ → V v = V' (σ✝ v)
h4 : ∀ v ∈ binders✝, v = σ✝ v
⊢ Holds D I V E (phi✝.imp_ psi✝) ↔ Holds D I V' E (phi'✝.imp_ psi'✝)

case and_
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ✝ : VarName → VarName
binders✝ : Finset VarName
phi✝ psi✝ phi'✝ psi'✝ : Formula
a✝¹ : IsSubAux σ✝ binders✝ phi✝ phi'✝
a✝ : IsSubAux σ✝ binders✝ psi✝ psi'✝
a_ih✝¹ :
  ∀ (V V' : VarAssignment D),
    (∀ v ∈ binders✝, V v = V' (σ✝ v)) →
      (∀ (v : VarName), σ✝ v ∉ binders✝ → V v = V' (σ✝ v)) →
        (∀ v ∈ binders✝, v = σ✝ v) → (Holds D I V E phi✝ ↔ Holds D I V' E phi'✝)
a_ih✝ :
  ∀ (V V' : VarAssignment D),
    (∀ v ∈ binders✝, V v = V' (σ✝ v)) →
      (∀ (v : VarName), σ✝ v ∉ binders✝ → V v = V' (σ✝ v)) →
        (∀ v ∈ binders✝, v = σ✝ v) → (Holds D I V E psi✝ ↔ Holds D I V' E psi'✝)
V V' : VarAssignment D
h2 : ∀ v ∈ binders✝, V v = V' (σ✝ v)
h3 : ∀ (v : VarName), σ✝ v ∉ binders✝ → V v = V' (σ✝ v)
h4 : ∀ v ∈ binders✝, v = σ✝ v
⊢ Holds D I V E (phi✝.and_ psi✝) ↔ Holds D I V' E (phi'✝.and_ psi'✝)

case or_
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ✝ : VarName → VarName
binders✝ : Finset VarName
phi✝ psi✝ phi'✝ psi'✝ : Formula
a✝¹ : IsSubAux σ✝ binders✝ phi✝ phi'✝
a✝ : IsSubAux σ✝ binders✝ psi✝ psi'✝
a_ih✝¹ :
  ∀ (V V' : VarAssignment D),
    (∀ v ∈ binders✝, V v = V' (σ✝ v)) →
      (∀ (v : VarName), σ✝ v ∉ binders✝ → V v = V' (σ✝ v)) →
        (∀ v ∈ binders✝, v = σ✝ v) → (Holds D I V E phi✝ ↔ Holds D I V' E phi'✝)
a_ih✝ :
  ∀ (V V' : VarAssignment D),
    (∀ v ∈ binders✝, V v = V' (σ✝ v)) →
      (∀ (v : VarName), σ✝ v ∉ binders✝ → V v = V' (σ✝ v)) →
        (∀ v ∈ binders✝, v = σ✝ v) → (Holds D I V E psi✝ ↔ Holds D I V' E psi'✝)
V V' : VarAssignment D
h2 : ∀ v ∈ binders✝, V v = V' (σ✝ v)
h3 : ∀ (v : VarName), σ✝ v ∉ binders✝ → V v = V' (σ✝ v)
h4 : ∀ v ∈ binders✝, v = σ✝ v
⊢ Holds D I V E (phi✝.or_ psi✝) ↔ Holds D I V' E (phi'✝.or_ psi'✝)

case iff_
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ✝ : VarName → VarName
binders✝ : Finset VarName
phi✝ psi✝ phi'✝ psi'✝ : Formula
a✝¹ : IsSubAux σ✝ binders✝ phi✝ phi'✝
a✝ : IsSubAux σ✝ binders✝ psi✝ psi'✝
a_ih✝¹ :
  ∀ (V V' : VarAssignment D),
    (∀ v ∈ binders✝, V v = V' (σ✝ v)) →
      (∀ (v : VarName), σ✝ v ∉ binders✝ → V v = V' (σ✝ v)) →
        (∀ v ∈ binders✝, v = σ✝ v) → (Holds D I V E phi✝ ↔ Holds D I V' E phi'✝)
a_ih✝ :
  ∀ (V V' : VarAssignment D),
    (∀ v ∈ binders✝, V v = V' (σ✝ v)) →
      (∀ (v : VarName), σ✝ v ∉ binders✝ → V v = V' (σ✝ v)) →
        (∀ v ∈ binders✝, v = σ✝ v) → (Holds D I V E psi✝ ↔ Holds D I V' E psi'✝)
V V' : VarAssignment D
h2 : ∀ v ∈ binders✝, V v = V' (σ✝ v)
h3 : ∀ (v : VarName), σ✝ v ∉ binders✝ → V v = V' (σ✝ v)
h4 : ∀ v ∈ binders✝, v = σ✝ v
⊢ Holds D I V E (phi✝.iff_ psi✝) ↔ Holds D I V' E (phi'✝.iff_ psi'✝)

case forall_
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ✝ : VarName → VarName
binders✝ : Finset VarName
x✝ : VarName
phi✝ phi'✝ : Formula
a✝ : IsSubAux (Function.updateITE σ✝ x✝ x✝) (binders✝ ∪ {x✝}) phi✝ phi'✝
a_ih✝ :
  ∀ (V V' : VarAssignment D),
    (∀ v ∈ binders✝ ∪ {x✝}, V v = V' (Function.updateITE σ✝ x✝ x✝ v)) →
      (∀ (v : VarName), Function.updateITE σ✝ x✝ x✝ v ∉ binders✝ ∪ {x✝} → V v = V' (Function.updateITE σ✝ x✝ x✝ v)) →
        (∀ v ∈ binders✝ ∪ {x✝}, v = Function.updateITE σ✝ x✝ x✝ v) → (Holds D I V E phi✝ ↔ Holds D I V' E phi'✝)
V V' : VarAssignment D
h2 : ∀ v ∈ binders✝, V v = V' (σ✝ v)
h3 : ∀ (v : VarName), σ✝ v ∉ binders✝ → V v = V' (σ✝ v)
h4 : ∀ v ∈ binders✝, v = σ✝ v
⊢ Holds D I V E (forall_ x✝ phi✝) ↔ Holds D I V' E (forall_ x✝ phi'✝)

case exists_
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ✝ : VarName → VarName
binders✝ : Finset VarName
x✝ : VarName
phi✝ phi'✝ : Formula
a✝ : IsSubAux (Function.updateITE σ✝ x✝ x✝) (binders✝ ∪ {x✝}) phi✝ phi'✝
a_ih✝ :
  ∀ (V V' : VarAssignment D),
    (∀ v ∈ binders✝ ∪ {x✝}, V v = V' (Function.updateITE σ✝ x✝ x✝ v)) →
      (∀ (v : VarName), Function.updateITE σ✝ x✝ x✝ v ∉ binders✝ ∪ {x✝} → V v = V' (Function.updateITE σ✝ x✝ x✝ v)) →
        (∀ v ∈ binders✝ ∪ {x✝}, v = Function.updateITE σ✝ x✝ x✝ v) → (Holds D I V E phi✝ ↔ Holds D I V' E phi'✝)
V V' : VarAssignment D
h2 : ∀ v ∈ binders✝, V v = V' (σ✝ v)
h3 : ∀ (v : VarName), σ✝ v ∉ binders✝ → V v = V' (σ✝ v)
h4 : ∀ v ∈ binders✝, v = σ✝ v
⊢ Holds D I V E (exists_ x✝ phi✝) ↔ Holds D I V' E (exists_ x✝ phi'✝)

case def_
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
binders : Finset VarName
F F' : Formula
σ✝ : VarName → VarName
binders✝ : Finset VarName
X✝ : DefName
xs✝ : List VarName
a✝ : ∀ v ∈ xs✝, v ∉ binders✝ → σ✝ v ∉ binders✝
V V' : VarAssignment D
h2 : ∀ v ∈ binders✝, V v = V' (σ✝ v)
h3 : ∀ (v : VarName), σ✝ v ∉ binders✝ → V v = V' (σ✝ v)
h4 : ∀ v ∈ binders✝, v = σ✝ v
⊢ Holds D I V E (def_ X✝ xs✝) ↔ Holds D I V' E (def_ X✝ (List.map σ✝ xs✝))