Theorem: FOL.NV.Sub.Var.All.Rec.Inj.substitution_theorem (FOL/NV/Sub/Var/All/Rec/Inj/ReplaceAll.lean)

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
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✝))

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]
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✝))

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]
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✝))

State before:
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
X : PredName
xs : List VarName
V : VarAssignment D
⊢ I.pred_var_ X (List.map (V ∘ σ) xs) ↔ I.pred_var_ X (List.map V (List.map σ xs))
Tactic:
case pred_const_ X xs | pred_var_ X xs =>
  simp
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
x y : VarName
V : VarAssignment D
⊢ (V ∘ σ) x = (V ∘ σ) y ↔ V (σ x) = V (σ y)
Tactic:
case eq_ x y =>
  simp
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
phi : Formula
phi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
V : VarAssignment D
⊢ ¬Holds D I (V ∘ σ) E phi ↔ ¬Holds D I V E (replaceAll σ phi)
Tactic:
case not_ phi phi_ih =>
  congr! 1
  exact phi_ih V
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
V : VarAssignment D
⊢ (∃ d, Holds D I (Function.updateITE (V ∘ σ) x d) E phi) ↔
    ∃ d, Holds D I (Function.updateITE V (σ x) d) E (replaceAll σ phi)
Tactic:
case forall_ x phi phi_ih | exists_ x phi phi_ih =>
  first | apply forall_congr' | apply exists_congr
  intro a
  have s1 : Function.updateITE V (σ x) a ∘ σ = Function.updateITE (V ∘ σ) x a
  apply Function.updateITE_comp_right_injective
  apply h1
  simp only [← s1]
  exact phi_ih (Function.updateITE V (σ x) a)
State after:
no goals

State before:
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:
simp only [replaceAll]
State after:
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✝))

State before:
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✝))
Tactic:
simp only [Holds]
State after:
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✝)

State before:
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
X : PredName
xs : List VarName
V : VarAssignment D
⊢ I.pred_var_ X (List.map (V ∘ σ) xs) ↔ I.pred_var_ X (List.map V (List.map σ xs))
Tactic:
simp
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
x y : VarName
V : VarAssignment D
⊢ (V ∘ σ) x = (V ∘ σ) y ↔ V (σ x) = V (σ y)
Tactic:
simp
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
phi : Formula
phi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
V : VarAssignment D
⊢ ¬Holds D I (V ∘ σ) E phi ↔ ¬Holds D I V E (replaceAll σ phi)
Tactic:
congr! 1
State after:
case a.h.e'_1.a
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
phi : Formula
phi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
V : VarAssignment D
⊢ Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)

State before:
case a.h.e'_1.a
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
phi : Formula
phi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
V : VarAssignment D
⊢ Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
Tactic:
exact phi_ih V
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
phi psi : Formula
phi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
psi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E psi ↔ Holds D I V E (replaceAll σ psi)
V : VarAssignment D
⊢ (Holds D I (V ∘ σ) E phi ↔ Holds D I (V ∘ σ) E psi) ↔
    (Holds D I V E (replaceAll σ phi) ↔ Holds D I V E (replaceAll σ psi))
Tactic:
congr! 1
State after:
case a.h.e'_1.a
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
phi psi : Formula
phi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
psi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E psi ↔ Holds D I V E (replaceAll σ psi)
V : VarAssignment D
⊢ Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)

case a.h.e'_2.a
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
phi psi : Formula
phi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
psi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E psi ↔ Holds D I V E (replaceAll σ psi)
V : VarAssignment D
⊢ Holds D I (V ∘ σ) E psi ↔ Holds D I V E (replaceAll σ psi)

State before:
case a.h.e'_1.a
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
phi psi : Formula
phi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
psi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E psi ↔ Holds D I V E (replaceAll σ psi)
V : VarAssignment D
⊢ Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
Tactic:
exact phi_ih V
State after:
no goals

State before:
case a.h.e'_2.a
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
phi psi : Formula
phi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
psi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E psi ↔ Holds D I V E (replaceAll σ psi)
V : VarAssignment D
⊢ Holds D I (V ∘ σ) E psi ↔ Holds D I V E (replaceAll σ psi)
Tactic:
exact psi_ih V
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
V : VarAssignment D
⊢ (∃ d, Holds D I (Function.updateITE (V ∘ σ) x d) E phi) ↔
    ∃ d, Holds D I (Function.updateITE V (σ x) d) E (replaceAll σ phi)
Tactic:
first | apply forall_congr' | apply exists_congr
State after:
case h
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
V : VarAssignment D
⊢ ∀ (a : D),
    Holds D I (Function.updateITE (V ∘ σ) x a) E phi ↔ Holds D I (Function.updateITE V (σ x) a) E (replaceAll σ phi)

State before:
case h
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
V : VarAssignment D
⊢ ∀ (a : D),
    Holds D I (Function.updateITE (V ∘ σ) x a) E phi ↔ Holds D I (Function.updateITE V (σ x) a) E (replaceAll σ phi)
Tactic:
intro a
State after:
case h
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
V : VarAssignment D
a : D
⊢ Holds D I (Function.updateITE (V ∘ σ) x a) E phi ↔ Holds D I (Function.updateITE V (σ x) a) E (replaceAll σ phi)

State before:
case h
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
V : VarAssignment D
a : D
⊢ Holds D I (Function.updateITE (V ∘ σ) x a) E phi ↔ Holds D I (Function.updateITE V (σ x) a) E (replaceAll σ phi)
Tactic:
have s1 : Function.updateITE V (σ x) a ∘ σ = Function.updateITE (V ∘ σ) x a
State after:
case s1
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
V : VarAssignment D
a : D
⊢ Function.updateITE V (σ x) a ∘ σ = Function.updateITE (V ∘ σ) x a

case h
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
V : VarAssignment D
a : D
s1 : Function.updateITE V (σ x) a ∘ σ = Function.updateITE (V ∘ σ) x a
⊢ Holds D I (Function.updateITE (V ∘ σ) x a) E phi ↔ Holds D I (Function.updateITE V (σ x) a) E (replaceAll σ phi)

State before:
case s1
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
V : VarAssignment D
a : D
⊢ Function.updateITE V (σ x) a ∘ σ = Function.updateITE (V ∘ σ) x a

case h
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
V : VarAssignment D
a : D
s1 : Function.updateITE V (σ x) a ∘ σ = Function.updateITE (V ∘ σ) x a
⊢ Holds D I (Function.updateITE (V ∘ σ) x a) E phi ↔ Holds D I (Function.updateITE V (σ x) a) E (replaceAll σ phi)
Tactic:
apply Function.updateITE_comp_right_injective
State after:
case s1.h1
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
V : VarAssignment D
a : D
⊢ Function.Injective σ

case h
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
V : VarAssignment D
a : D
s1 : Function.updateITE V (σ x) a ∘ σ = Function.updateITE (V ∘ σ) x a
⊢ Holds D I (Function.updateITE (V ∘ σ) x a) E phi ↔ Holds D I (Function.updateITE V (σ x) a) E (replaceAll σ phi)

State before:
case s1.h1
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
V : VarAssignment D
a : D
⊢ Function.Injective σ

case h
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
V : VarAssignment D
a : D
s1 : Function.updateITE V (σ x) a ∘ σ = Function.updateITE (V ∘ σ) x a
⊢ Holds D I (Function.updateITE (V ∘ σ) x a) E phi ↔ Holds D I (Function.updateITE V (σ x) a) E (replaceAll σ phi)
Tactic:
apply h1
State after:
case h
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
V : VarAssignment D
a : D
s1 : Function.updateITE V (σ x) a ∘ σ = Function.updateITE (V ∘ σ) x a
⊢ Holds D I (Function.updateITE (V ∘ σ) x a) E phi ↔ Holds D I (Function.updateITE V (σ x) a) E (replaceAll σ phi)

State before:
case h
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
V : VarAssignment D
a : D
s1 : Function.updateITE V (σ x) a ∘ σ = Function.updateITE (V ∘ σ) x a
⊢ Holds D I (Function.updateITE (V ∘ σ) x a) E phi ↔ Holds D I (Function.updateITE V (σ x) a) E (replaceAll σ phi)
Tactic:
simp only [← s1]
State after:
case h
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
V : VarAssignment D
a : D
s1 : Function.updateITE V (σ x) a ∘ σ = Function.updateITE (V ∘ σ) x a
⊢ Holds D I (Function.updateITE V (σ x) a ∘ σ) E phi ↔ Holds D I (Function.updateITE V (σ x) a) E (replaceAll σ phi)

State before:
case h
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
V : VarAssignment D
a : D
s1 : Function.updateITE V (σ x) a ∘ σ = Function.updateITE (V ∘ σ) x a
⊢ Holds D I (Function.updateITE V (σ x) a ∘ σ) E phi ↔ Holds D I (Function.updateITE V (σ x) a) E (replaceAll σ phi)
Tactic:
exact phi_ih (Function.updateITE V (σ x) a)
State after:
no goals

State before:
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
V : VarAssignment D
⊢ (∀ (d : D), Holds D I (Function.updateITE (V ∘ σ) x d) E phi) ↔
    ∀ (d : D), Holds D I (Function.updateITE V (σ x) d) E (replaceAll σ phi)
Tactic:
apply forall_congr'
State after:
case h
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
V : VarAssignment D
⊢ ∀ (a : D),
    Holds D I (Function.updateITE (V ∘ σ) x a) E phi ↔ Holds D I (Function.updateITE V (σ x) a) E (replaceAll σ phi)

State before:
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
V : VarAssignment D
⊢ (∃ d, Holds D I (Function.updateITE (V ∘ σ) x d) E phi) ↔
    ∃ d, Holds D I (Function.updateITE V (σ x) d) E (replaceAll σ phi)
Tactic:
apply exists_congr
State after:
case h
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
x : VarName
phi : Formula
phi_ih : ∀ (V : VarAssignment D), Holds D I (V ∘ σ) E phi ↔ Holds D I V E (replaceAll σ phi)
V : VarAssignment D
⊢ ∀ (a : D),
    Holds D I (Function.updateITE (V ∘ σ) x a) E phi ↔ Holds D I (Function.updateITE V (σ x) a) E (replaceAll σ phi)

State before:
D : Type
I : Interpretation D
E : Env
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
⊢ Holds D I (V ∘ σ) E (def_ X xs) ↔ Holds D I V E (def_ X (List.map σ xs))
Tactic:
induction E
State after:
case nil
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
⊢ Holds D I (V ∘ σ) [] (def_ X xs) ↔ Holds D I V [] (def_ X (List.map σ xs))

case cons
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
head✝ : Definition
tail✝ : List Definition
tail_ih✝ : Holds D I (V ∘ σ) tail✝ (def_ X xs) ↔ Holds D I V tail✝ (def_ X (List.map σ xs))
⊢ Holds D I (V ∘ σ) (head✝ :: tail✝) (def_ X xs) ↔ Holds D I V (head✝ :: tail✝) (def_ X (List.map σ xs))

State before:
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
⊢ Holds D I (V ∘ σ) [] (def_ X xs) ↔ Holds D I V [] (def_ X (List.map σ xs))
Tactic:
case nil =>
  simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
⊢ Holds D I (V ∘ σ) [] (def_ X xs) ↔ Holds D I V [] (def_ X (List.map σ xs))
Tactic:
simp only [Holds]
State after:
no goals

State before:
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
⊢ Holds D I (V ∘ σ) (E_hd :: E_tl) (def_ X xs) ↔ Holds D I V (E_hd :: E_tl) (def_ X (List.map σ xs))
Tactic:
simp only [Holds]
State after:
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
⊢ (if X = E_hd.name ∧ xs.length = E_hd.args.length then
      Holds D I (Function.updateListITE (V ∘ σ) E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q
    else Holds D I (V ∘ σ) E_tl (def_ X xs)) ↔
    if X = E_hd.name ∧ (List.map σ xs).length = E_hd.args.length then
      Holds D I (Function.updateListITE V E_hd.args (List.map V (List.map σ xs))) E_tl E_hd.q
    else Holds D I V E_tl (def_ X (List.map σ xs))

State before:
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
⊢ (if X = E_hd.name ∧ xs.length = E_hd.args.length then
      Holds D I (Function.updateListITE (V ∘ σ) E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q
    else Holds D I (V ∘ σ) E_tl (def_ X xs)) ↔
    if X = E_hd.name ∧ (List.map σ xs).length = E_hd.args.length then
      Holds D I (Function.updateListITE V E_hd.args (List.map V (List.map σ xs))) E_tl E_hd.q
    else Holds D I V E_tl (def_ X (List.map σ xs))
Tactic:
simp
State after:
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
⊢ (if X = E_hd.name ∧ xs.length = E_hd.args.length then
      Holds D I (Function.updateListITE (V ∘ σ) E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q
    else Holds D I (V ∘ σ) E_tl (def_ X xs)) ↔
    if X = E_hd.name ∧ xs.length = E_hd.args.length then
      Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q
    else Holds D I V E_tl (def_ X (List.map σ xs))

State before:
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
⊢ (if X = E_hd.name ∧ xs.length = E_hd.args.length then
      Holds D I (Function.updateListITE (V ∘ σ) E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q
    else Holds D I (V ∘ σ) E_tl (def_ X xs)) ↔
    if X = E_hd.name ∧ xs.length = E_hd.args.length then
      Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q
    else Holds D I V E_tl (def_ X (List.map σ xs))
Tactic:
split_ifs
State after:
case pos
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
h✝ : X = E_hd.name ∧ xs.length = E_hd.args.length
⊢ Holds D I (Function.updateListITE (V ∘ σ) E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q ↔
    Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q

case neg
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
h✝ : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
⊢ Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))

State before:
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
⊢ Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
Tactic:
case _ c1 =>
  apply E_ih
State after:
no goals

State before:
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
c1 : X = E_hd.name ∧ xs.length = E_hd.args.length
⊢ Holds D I (Function.updateListITE (V ∘ σ) E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q ↔
    Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q
Tactic:
cases c1
State after:
case intro
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
left✝ : X = E_hd.name
right✝ : xs.length = E_hd.args.length
⊢ Holds D I (Function.updateListITE (V ∘ σ) E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q ↔
    Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q

State before:
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
⊢ Holds D I (Function.updateListITE (V ∘ σ) E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q ↔
    Holds D I (Function.updateListITE V E_hd.args (List.map (V ∘ σ) xs)) E_tl E_hd.q
Tactic:
apply Holds_coincide_Var
State after:
case h1
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
⊢ ∀ (v : VarName),
    isFreeIn v E_hd.q →
      Function.updateListITE (V ∘ σ) E_hd.args (List.map (V ∘ σ) xs) v =
        Function.updateListITE V E_hd.args (List.map (V ∘ σ) xs) v

State before:
case h1
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
⊢ ∀ (v : VarName),
    isFreeIn v E_hd.q →
      Function.updateListITE (V ∘ σ) E_hd.args (List.map (V ∘ σ) xs) v =
        Function.updateListITE V E_hd.args (List.map (V ∘ σ) xs) v
Tactic:
intro v a1
State after:
case h1
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
v : VarName
a1 : isFreeIn v E_hd.q
⊢ Function.updateListITE (V ∘ σ) E_hd.args (List.map (V ∘ σ) xs) v =
    Function.updateListITE V E_hd.args (List.map (V ∘ σ) xs) v

State before:
case h1
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
v : VarName
a1 : isFreeIn v E_hd.q
⊢ Function.updateListITE (V ∘ σ) E_hd.args (List.map (V ∘ σ) xs) v =
    Function.updateListITE V E_hd.args (List.map (V ∘ σ) xs) v
Tactic:
simp only [isFreeIn_iff_mem_freeVarSet v E_hd.q] at a1
State after:
case h1
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
v : VarName
a1 : v ∈ E_hd.q.freeVarSet
⊢ Function.updateListITE (V ∘ σ) E_hd.args (List.map (V ∘ σ) xs) v =
    Function.updateListITE V E_hd.args (List.map (V ∘ σ) xs) v

State before:
case h1
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
v : VarName
a1 : v ∈ E_hd.q.freeVarSet
⊢ Function.updateListITE (V ∘ σ) E_hd.args (List.map (V ∘ σ) xs) v =
    Function.updateListITE V E_hd.args (List.map (V ∘ σ) xs) v
Tactic:
apply Function.updateListITE_mem_eq_len
State after:
case h1.h1
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
v : VarName
a1 : v ∈ E_hd.q.freeVarSet
⊢ v ∈ E_hd.args

case h1.h2
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
v : VarName
a1 : v ∈ E_hd.q.freeVarSet
⊢ E_hd.args.length = (List.map (V ∘ σ) xs).length

State before:
case h1.h1
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
v : VarName
a1 : v ∈ E_hd.q.freeVarSet
⊢ v ∈ E_hd.args
Tactic:
simp only [<- List.mem_toFinset]
State after:
case h1.h1
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
v : VarName
a1 : v ∈ E_hd.q.freeVarSet
⊢ v ∈ E_hd.args.toFinset

State before:
case h1.h1
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
v : VarName
a1 : v ∈ E_hd.q.freeVarSet
⊢ v ∈ E_hd.args.toFinset
Tactic:
apply Finset.mem_of_subset E_hd.h1 a1
State after:
no goals

State before:
case h1.h2
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
v : VarName
a1 : v ∈ E_hd.q.freeVarSet
⊢ E_hd.args.length = (List.map (V ∘ σ) xs).length
Tactic:
simp
State after:
case h1.h2
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
v : VarName
a1 : v ∈ E_hd.q.freeVarSet
⊢ E_hd.args.length = xs.length

State before:
case h1.h2
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
c1_left : X = E_hd.name
c1_right : xs.length = E_hd.args.length
v : VarName
a1 : v ∈ E_hd.q.freeVarSet
⊢ E_hd.args.length = xs.length
Tactic:
simp only [c1_right]
State after:
no goals

State before:
D : Type
I : Interpretation D
σ : VarName → VarName
h1 : Function.Injective σ
X : DefName
xs : List VarName
V : VarAssignment D
E_hd : Definition
E_tl : List Definition
E_ih : Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
c1 : ¬(X = E_hd.name ∧ xs.length = E_hd.args.length)
⊢ Holds D I (V ∘ σ) E_tl (def_ X xs) ↔ Holds D I V E_tl (def_ X (List.map σ xs))
Tactic:
apply E_ih
State after:
no goals