Theorem: FOL.NV.Sub.Var.All.Rec.Fresh.substitution_theorem
Proof state before:
D : Type
I : Interpretation D
V : VarAssignment D
E : Env
σ : VarName → VarName
c : Char
F : Formula
⊢ Holds D I V E (sub σ c F) ↔ Holds D I (V ∘ σ) E F
Tactic:
induction F generalizing σ V
Proof state after:
case pred_const_
D : Type
I : Interpretation D
E : Env
c : Char
a✝¹ : PredName
a✝ : List VarName
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c (pred_const_ a✝¹ a✝)) ↔ Holds D I (V ∘ σ) E (pred_const_ a✝¹ a✝)

case pred_var_
D : Type
I : Interpretation D
E : Env
c : Char
a✝¹ : PredName
a✝ : List VarName
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c (pred_var_ a✝¹ a✝)) ↔ Holds D I (V ∘ σ) E (pred_var_ a✝¹ a✝)

case eq_
D : Type
I : Interpretation D
E : Env
c : Char
a✝¹ a✝ : VarName
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c (eq_ a✝¹ a✝)) ↔ Holds D I (V ∘ σ) E (eq_ a✝¹ a✝)

case true_
D : Type
I : Interpretation D
E : Env
c : Char
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c true_) ↔ Holds D I (V ∘ σ) E true_

case false_
D : Type
I : Interpretation D
E : Env
c : Char
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c false_) ↔ Holds D I (V ∘ σ) E false_

case not_
D : Type
I : Interpretation D
E : Env
c : Char
a✝ : Formula
a_ih✝ : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c a✝) ↔ Holds D I (V ∘ σ) E a✝
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c a✝.not_) ↔ Holds D I (V ∘ σ) E a✝.not_

case imp_
D : Type
I : Interpretation D
E : Env
c : Char
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c a✝¹) ↔ Holds D I (V ∘ σ) E a✝¹
a_ih✝ : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c a✝) ↔ Holds D I (V ∘ σ) E a✝
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c (a✝¹.imp_ a✝)) ↔ Holds D I (V ∘ σ) E (a✝¹.imp_ a✝)

case and_
D : Type
I : Interpretation D
E : Env
c : Char
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c a✝¹) ↔ Holds D I (V ∘ σ) E a✝¹
a_ih✝ : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c a✝) ↔ Holds D I (V ∘ σ) E a✝
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c (a✝¹.and_ a✝)) ↔ Holds D I (V ∘ σ) E (a✝¹.and_ a✝)

case or_
D : Type
I : Interpretation D
E : Env
c : Char
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c a✝¹) ↔ Holds D I (V ∘ σ) E a✝¹
a_ih✝ : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c a✝) ↔ Holds D I (V ∘ σ) E a✝
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c (a✝¹.or_ a✝)) ↔ Holds D I (V ∘ σ) E (a✝¹.or_ a✝)

case iff_
D : Type
I : Interpretation D
E : Env
c : Char
a✝¹ a✝ : Formula
a_ih✝¹ : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c a✝¹) ↔ Holds D I (V ∘ σ) E a✝¹
a_ih✝ : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c a✝) ↔ Holds D I (V ∘ σ) E a✝
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c (a✝¹.iff_ a✝)) ↔ Holds D I (V ∘ σ) E (a✝¹.iff_ a✝)

case forall_
D : Type
I : Interpretation D
E : Env
c : Char
a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c a✝) ↔ Holds D I (V ∘ σ) E a✝
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c (forall_ a✝¹ a✝)) ↔ Holds D I (V ∘ σ) E (forall_ a✝¹ a✝)

case exists_
D : Type
I : Interpretation D
E : Env
c : Char
a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c a✝) ↔ Holds D I (V ∘ σ) E a✝
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c (exists_ a✝¹ a✝)) ↔ Holds D I (V ∘ σ) E (exists_ a✝¹ a✝)

case def_
D : Type
I : Interpretation D
E : Env
c : Char
a✝¹ : DefName
a✝ : List VarName
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c (def_ a✝¹ a✝)) ↔ Holds D I (V ∘ σ) E (def_ a✝¹ a✝)