Theorem: FOL.NV.Sub.Var.All.Rec.Inj.substitution_theorem
Proof state before:
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✝))
Tactic:
all_goals
  simp only [replaceAll]
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 (pred_const_ a✝¹ (List.map σ 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 (pred_var_ a✝¹ (List.map σ 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 (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 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 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_ (replaceAll σ 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_ (replaceAll σ 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_ (replaceAll σ 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_ (replaceAll σ 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 (forall_ (σ a✝¹) (replaceAll σ 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 (exists_ (σ a✝¹) (replaceAll σ 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 (def_ a✝¹ (List.map σ a✝))