Theorem: FOL.NV.Sub.Var.All.Rec.fastReplaceFree_same_on_free
Proof state before:
case pred_const_
a✝¹ : PredName
a✝ : List VarName
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v (pred_const_ a✝¹ a✝) → σ v = σ' v
⊢ fastReplaceFree σ (pred_const_ a✝¹ a✝) = fastReplaceFree σ' (pred_const_ a✝¹ a✝)

case pred_var_
a✝¹ : PredName
a✝ : List VarName
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v (pred_var_ a✝¹ a✝) → σ v = σ' v
⊢ fastReplaceFree σ (pred_var_ a✝¹ a✝) = fastReplaceFree σ' (pred_var_ a✝¹ a✝)

case eq_
a✝¹ a✝ : VarName
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v (eq_ a✝¹ a✝) → σ v = σ' v
⊢ fastReplaceFree σ (eq_ a✝¹ a✝) = fastReplaceFree σ' (eq_ a✝¹ a✝)

case true_
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v true_ → σ v = σ' v
⊢ fastReplaceFree σ true_ = fastReplaceFree σ' true_

case false_
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v false_ → σ v = σ' v
⊢ fastReplaceFree σ false_ = fastReplaceFree σ' false_

case not_
a✝ : Formula
a_ih✝ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝ → σ v = σ' v) → fastReplaceFree σ a✝ = fastReplaceFree σ' a✝
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v a✝.not_ → σ v = σ' v
⊢ fastReplaceFree σ a✝.not_ = fastReplaceFree σ' a✝.not_

case imp_
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝¹ → σ v = σ' v) → fastReplaceFree σ a✝¹ = fastReplaceFree σ' a✝¹
a_ih✝ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝ → σ v = σ' v) → fastReplaceFree σ a✝ = fastReplaceFree σ' a✝
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v (a✝¹.imp_ a✝) → σ v = σ' v
⊢ fastReplaceFree σ (a✝¹.imp_ a✝) = fastReplaceFree σ' (a✝¹.imp_ a✝)

case and_
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝¹ → σ v = σ' v) → fastReplaceFree σ a✝¹ = fastReplaceFree σ' a✝¹
a_ih✝ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝ → σ v = σ' v) → fastReplaceFree σ a✝ = fastReplaceFree σ' a✝
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v (a✝¹.and_ a✝) → σ v = σ' v
⊢ fastReplaceFree σ (a✝¹.and_ a✝) = fastReplaceFree σ' (a✝¹.and_ a✝)

case or_
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝¹ → σ v = σ' v) → fastReplaceFree σ a✝¹ = fastReplaceFree σ' a✝¹
a_ih✝ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝ → σ v = σ' v) → fastReplaceFree σ a✝ = fastReplaceFree σ' a✝
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v (a✝¹.or_ a✝) → σ v = σ' v
⊢ fastReplaceFree σ (a✝¹.or_ a✝) = fastReplaceFree σ' (a✝¹.or_ a✝)

case iff_
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝¹ → σ v = σ' v) → fastReplaceFree σ a✝¹ = fastReplaceFree σ' a✝¹
a_ih✝ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝ → σ v = σ' v) → fastReplaceFree σ a✝ = fastReplaceFree σ' a✝
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v (a✝¹.iff_ a✝) → σ v = σ' v
⊢ fastReplaceFree σ (a✝¹.iff_ a✝) = fastReplaceFree σ' (a✝¹.iff_ a✝)

case forall_
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝ → σ v = σ' v) → fastReplaceFree σ a✝ = fastReplaceFree σ' a✝
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v (forall_ a✝¹ a✝) → σ v = σ' v
⊢ fastReplaceFree σ (forall_ a✝¹ a✝) = fastReplaceFree σ' (forall_ a✝¹ a✝)

case exists_
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝ → σ v = σ' v) → fastReplaceFree σ a✝ = fastReplaceFree σ' a✝
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v (exists_ a✝¹ a✝) → σ v = σ' v
⊢ fastReplaceFree σ (exists_ a✝¹ a✝) = fastReplaceFree σ' (exists_ a✝¹ a✝)

case def_
a✝¹ : DefName
a✝ : List VarName
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v (def_ a✝¹ a✝) → σ v = σ' v
⊢ fastReplaceFree σ (def_ a✝¹ a✝) = fastReplaceFree σ' (def_ a✝¹ a✝)
Tactic:
all_goals
  simp only [isFreeIn] at h1
  simp only [fastReplaceFree]
Proof state after:
case pred_const_
a✝¹ : PredName
a✝ : List VarName
σ σ' : VarName → VarName
h1 : ∀ v ∈ a✝, σ v = σ' v
⊢ pred_const_ a✝¹ (List.map σ a✝) = pred_const_ a✝¹ (List.map σ' a✝)

case pred_var_
a✝¹ : PredName
a✝ : List VarName
σ σ' : VarName → VarName
h1 : ∀ v ∈ a✝, σ v = σ' v
⊢ pred_var_ a✝¹ (List.map σ a✝) = pred_var_ a✝¹ (List.map σ' a✝)

case eq_
a✝¹ a✝ : VarName
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), v = a✝¹ ∨ v = a✝ → σ v = σ' v
⊢ eq_ (σ a✝¹) (σ a✝) = eq_ (σ' a✝¹) (σ' a✝)

case not_
a✝ : Formula
a_ih✝ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝ → σ v = σ' v) → fastReplaceFree σ a✝ = fastReplaceFree σ' a✝
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v a✝ → σ v = σ' v
⊢ (fastReplaceFree σ a✝).not_ = (fastReplaceFree σ' a✝).not_

case imp_
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝¹ → σ v = σ' v) → fastReplaceFree σ a✝¹ = fastReplaceFree σ' a✝¹
a_ih✝ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝ → σ v = σ' v) → fastReplaceFree σ a✝ = fastReplaceFree σ' a✝
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v a✝¹ ∨ isFreeIn v a✝ → σ v = σ' v
⊢ (fastReplaceFree σ a✝¹).imp_ (fastReplaceFree σ a✝) = (fastReplaceFree σ' a✝¹).imp_ (fastReplaceFree σ' a✝)

case and_
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝¹ → σ v = σ' v) → fastReplaceFree σ a✝¹ = fastReplaceFree σ' a✝¹
a_ih✝ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝ → σ v = σ' v) → fastReplaceFree σ a✝ = fastReplaceFree σ' a✝
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v a✝¹ ∨ isFreeIn v a✝ → σ v = σ' v
⊢ (fastReplaceFree σ a✝¹).and_ (fastReplaceFree σ a✝) = (fastReplaceFree σ' a✝¹).and_ (fastReplaceFree σ' a✝)

case or_
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝¹ → σ v = σ' v) → fastReplaceFree σ a✝¹ = fastReplaceFree σ' a✝¹
a_ih✝ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝ → σ v = σ' v) → fastReplaceFree σ a✝ = fastReplaceFree σ' a✝
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v a✝¹ ∨ isFreeIn v a✝ → σ v = σ' v
⊢ (fastReplaceFree σ a✝¹).or_ (fastReplaceFree σ a✝) = (fastReplaceFree σ' a✝¹).or_ (fastReplaceFree σ' a✝)

case iff_
a✝¹ a✝ : Formula
a_ih✝¹ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝¹ → σ v = σ' v) → fastReplaceFree σ a✝¹ = fastReplaceFree σ' a✝¹
a_ih✝ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝ → σ v = σ' v) → fastReplaceFree σ a✝ = fastReplaceFree σ' a✝
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v a✝¹ ∨ isFreeIn v a✝ → σ v = σ' v
⊢ (fastReplaceFree σ a✝¹).iff_ (fastReplaceFree σ a✝) = (fastReplaceFree σ' a✝¹).iff_ (fastReplaceFree σ' a✝)

case forall_
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝ → σ v = σ' v) → fastReplaceFree σ a✝ = fastReplaceFree σ' a✝
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), ¬v = a✝¹ ∧ isFreeIn v a✝ → σ v = σ' v
⊢ forall_ a✝¹ (fastReplaceFree (Function.updateITE σ a✝¹ a✝¹) a✝) =
    forall_ a✝¹ (fastReplaceFree (Function.updateITE σ' a✝¹ a✝¹) a✝)

case exists_
a✝¹ : VarName
a✝ : Formula
a_ih✝ :
  ∀ (σ σ' : VarName → VarName),
    (∀ (v : VarName), isFreeIn v a✝ → σ v = σ' v) → fastReplaceFree σ a✝ = fastReplaceFree σ' a✝
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), ¬v = a✝¹ ∧ isFreeIn v a✝ → σ v = σ' v
⊢ exists_ a✝¹ (fastReplaceFree (Function.updateITE σ a✝¹ a✝¹) a✝) =
    exists_ a✝¹ (fastReplaceFree (Function.updateITE σ' a✝¹ a✝¹) a✝)

case def_
a✝¹ : DefName
a✝ : List VarName
σ σ' : VarName → VarName
h1 : ∀ v ∈ a✝, σ v = σ' v
⊢ def_ a✝¹ (List.map σ a✝) = def_ a✝¹ (List.map σ' a✝)