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

case pred_var_
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
a✝¹ : PredName
a✝ : List VarName
V : VarAssignment D
⊢ Holds D I (V ∘ σ) E (pred_var_ a✝¹ a✝) ↔ Holds D I V E (replaceAll σ (pred_var_ a✝¹ a✝))

case eq_
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
a✝¹ a✝ : VarName
V : VarAssignment D
⊢ Holds D I (V ∘ σ) E (eq_ a✝¹ a✝) ↔ Holds D I V E (replaceAll σ (eq_ a✝¹ a✝))

case true_
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
V : VarAssignment D
⊢ Holds D I (V ∘ σ) E true_ ↔ Holds D I V E (replaceAll σ true_)

case false_
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
V : VarAssignment D
⊢ Holds D I (V ∘ σ) E false_ ↔ Holds D I V E (replaceAll σ false_)

case not_
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
a✝ : Formula
a_ih✝ : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E a✝ ↔ Holds D I V E (replaceAll σ a✝)
V : VarAssignment D
⊢ Holds D I (V ∘ σ) E a✝.not_ ↔ Holds D I V E (replaceAll σ a✝.not_)

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

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

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

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

case forall_
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E a✝ ↔ Holds D I V E (replaceAll σ a✝)
V : VarAssignment D
⊢ Holds D I (V ∘ σ) E (forall_ a✝¹ a✝) ↔ Holds D I V E (replaceAll σ (forall_ a✝¹ a✝))

case exists_
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
a✝¹ : VarName
a✝ : Formula
a_ih✝ : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E a✝ ↔ Holds D I V E (replaceAll σ a✝)
V : VarAssignment D
⊢ Holds D I (V ∘ σ) E (exists_ a✝¹ a✝) ↔ Holds D I V E (replaceAll σ (exists_ a✝¹ a✝))

case def_
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
a✝¹ : DefName
a✝ : List VarName
V : VarAssignment D
⊢ Holds D I (V ∘ σ) E (def_ a✝¹ a✝) ↔ Holds D I V E (replaceAll σ (def_ a✝¹ a✝))