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 (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✝))
Tactic:
any_goals
  simp only [Holds]
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
⊢ I.pred_const_ a✝¹ (List.map (V ∘ σ) a✝) ↔ I.pred_const_ a✝¹ (List.map V (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
⊢ I.pred_var_ a✝¹ (List.map (V ∘ σ) a✝) ↔ I.pred_var_ a✝¹ (List.map V (List.map σ a✝))

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

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✝ ↔ ¬Holds D I V E (replaceAll σ a✝)

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✝¹ → Holds D I (V ∘ σ) E a✝ ↔ Holds D I V E (replaceAll σ a✝¹) → Holds D I V E (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✝¹ ∧ Holds D I (V ∘ σ) E a✝ ↔ Holds D I V E (replaceAll σ a✝¹) ∧ Holds D I V E (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✝¹ ∨ Holds D I (V ∘ σ) E a✝ ↔ Holds D I V E (replaceAll σ a✝¹) ∨ Holds D I V E (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✝¹ ↔ Holds D I (V ∘ σ) E a✝) ↔
    (Holds D I V E (replaceAll σ a✝¹) ↔ Holds D I V E (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
⊢ (∀ (d : D), Holds D I (Function.updateITE (V ∘ σ) a✝¹ d) E a✝) ↔
    ∀ (d : D), Holds D I (Function.updateITE V (σ a✝¹) d) E (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
⊢ (∃ d, Holds D I (Function.updateITE (V ∘ σ) a✝¹ d) E a✝) ↔
    ∃ d, Holds D I (Function.updateITE V (σ a✝¹) d) E (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✝))