Theorem: FOL.NV.Sub.Var.All.Rec.fastReplaceFree_same_on_free
Proof state before:
F : Formula
σ σ' : VarName → VarName
h1 : ∀ (v : VarName), isFreeIn v F → σ v = σ' v
⊢ fastReplaceFree σ F = fastReplaceFree σ' F
Tactic:
induction F generalizing σ σ'
Proof state after:
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✝)