Theorem: FOL.NV.Sub.Var.One.Ind.isFreeSub_imp_fastReplaceFree
Proof state before:
case pred_const_
F F' : Formula
v u : VarName
X✝ : PredName
xs✝ : List VarName
v✝ t✝ : VarName
⊢ Rec.fastReplaceFree v✝ t✝ (pred_const_ X✝ xs✝) = pred_const_ X✝ (List.map (fun x => if v✝ = x then t✝ else x) xs✝)

case pred_var_
F F' : Formula
v u : VarName
X✝ : PredName
xs✝ : List VarName
v✝ t✝ : VarName
⊢ Rec.fastReplaceFree v✝ t✝ (pred_var_ X✝ xs✝) = pred_var_ X✝ (List.map (fun x => if v✝ = x then t✝ else x) xs✝)

case eq_
F F' : Formula
v u x✝ y✝ v✝ t✝ : VarName
⊢ Rec.fastReplaceFree v✝ t✝ (eq_ x✝ y✝) = eq_ (if v✝ = x✝ then t✝ else x✝) (if v✝ = y✝ then t✝ else y✝)

case true_
F F' : Formula
v u v✝ t✝ : VarName
⊢ Rec.fastReplaceFree v✝ t✝ true_ = true_

case false_
F F' : Formula
v u v✝ t✝ : VarName
⊢ Rec.fastReplaceFree v✝ t✝ false_ = false_

case not_
F F' : Formula
v u : VarName
phi✝ : Formula
v✝ t✝ : VarName
phi'✝ : Formula
a✝ : IsSub phi✝ v✝ t✝ phi'✝
a_ih✝ : Rec.fastReplaceFree v✝ t✝ phi✝ = phi'✝
⊢ Rec.fastReplaceFree v✝ t✝ phi✝.not_ = phi'✝.not_

case imp_
F F' : Formula
v u : VarName
phi✝ psi✝ : Formula
v✝ t✝ : VarName
phi'✝ psi'✝ : Formula
a✝¹ : IsSub phi✝ v✝ t✝ phi'✝
a✝ : IsSub psi✝ v✝ t✝ psi'✝
a_ih✝¹ : Rec.fastReplaceFree v✝ t✝ phi✝ = phi'✝
a_ih✝ : Rec.fastReplaceFree v✝ t✝ psi✝ = psi'✝
⊢ Rec.fastReplaceFree v✝ t✝ (phi✝.imp_ psi✝) = phi'✝.imp_ psi'✝

case and_
F F' : Formula
v u : VarName
phi✝ psi✝ : Formula
v✝ t✝ : VarName
phi'✝ psi'✝ : Formula
a✝¹ : IsSub phi✝ v✝ t✝ phi'✝
a✝ : IsSub psi✝ v✝ t✝ psi'✝
a_ih✝¹ : Rec.fastReplaceFree v✝ t✝ phi✝ = phi'✝
a_ih✝ : Rec.fastReplaceFree v✝ t✝ psi✝ = psi'✝
⊢ Rec.fastReplaceFree v✝ t✝ (phi✝.and_ psi✝) = phi'✝.and_ psi'✝

case or_
F F' : Formula
v u : VarName
phi✝ psi✝ : Formula
v✝ t✝ : VarName
phi'✝ psi'✝ : Formula
a✝¹ : IsSub phi✝ v✝ t✝ phi'✝
a✝ : IsSub psi✝ v✝ t✝ psi'✝
a_ih✝¹ : Rec.fastReplaceFree v✝ t✝ phi✝ = phi'✝
a_ih✝ : Rec.fastReplaceFree v✝ t✝ psi✝ = psi'✝
⊢ Rec.fastReplaceFree v✝ t✝ (phi✝.or_ psi✝) = phi'✝.or_ psi'✝

case iff_
F F' : Formula
v u : VarName
phi✝ psi✝ : Formula
v✝ t✝ : VarName
phi'✝ psi'✝ : Formula
a✝¹ : IsSub phi✝ v✝ t✝ phi'✝
a✝ : IsSub psi✝ v✝ t✝ psi'✝
a_ih✝¹ : Rec.fastReplaceFree v✝ t✝ phi✝ = phi'✝
a_ih✝ : Rec.fastReplaceFree v✝ t✝ psi✝ = psi'✝
⊢ Rec.fastReplaceFree v✝ t✝ (phi✝.iff_ psi✝) = phi'✝.iff_ psi'✝

case forall_not_free_in
F F' : Formula
v u x✝ : VarName
phi✝ : Formula
v✝ t✝ : VarName
a✝ : ¬isFreeIn v✝ (forall_ x✝ phi✝)
⊢ Rec.fastReplaceFree v✝ t✝ (forall_ x✝ phi✝) = forall_ x✝ phi✝

case forall_free_in
F F' : Formula
v u x✝ : VarName
phi✝ : Formula
v✝ t✝ : VarName
phi'✝ : Formula
a✝² : isFreeIn v✝ (forall_ x✝ phi✝)
a✝¹ : ¬x✝ = t✝
a✝ : IsSub phi✝ v✝ t✝ phi'✝
a_ih✝ : Rec.fastReplaceFree v✝ t✝ phi✝ = phi'✝
⊢ Rec.fastReplaceFree v✝ t✝ (forall_ x✝ phi✝) = forall_ x✝ phi'✝

case exists_not_free_in
F F' : Formula
v u x✝ : VarName
phi✝ : Formula
v✝ t✝ : VarName
a✝ : ¬isFreeIn v✝ (exists_ x✝ phi✝)
⊢ Rec.fastReplaceFree v✝ t✝ (exists_ x✝ phi✝) = exists_ x✝ phi✝

case exists_free_in
F F' : Formula
v u x✝ : VarName
phi✝ : Formula
v✝ t✝ : VarName
phi'✝ : Formula
a✝² : isFreeIn v✝ (exists_ x✝ phi✝)
a✝¹ : ¬x✝ = t✝
a✝ : IsSub phi✝ v✝ t✝ phi'✝
a_ih✝ : Rec.fastReplaceFree v✝ t✝ phi✝ = phi'✝
⊢ Rec.fastReplaceFree v✝ t✝ (exists_ x✝ phi✝) = exists_ x✝ phi'✝

case def_
F F' : Formula
v u : VarName
X✝ : DefName
xs✝ : List VarName
v✝ t✝ : VarName
⊢ Rec.fastReplaceFree v✝ t✝ (def_ X✝ xs✝) = def_ X✝ (List.map (fun x => if v✝ = x then t✝ else x) xs✝)
Tactic:
all_goals
  simp only [Rec.fastReplaceFree]
Proof state after:
case not_
F F' : Formula
v u : VarName
phi✝ : Formula
v✝ t✝ : VarName
phi'✝ : Formula
a✝ : IsSub phi✝ v✝ t✝ phi'✝
a_ih✝ : Rec.fastReplaceFree v✝ t✝ phi✝ = phi'✝
⊢ (Rec.fastReplaceFree v✝ t✝ phi✝).not_ = phi'✝.not_

case imp_
F F' : Formula
v u : VarName
phi✝ psi✝ : Formula
v✝ t✝ : VarName
phi'✝ psi'✝ : Formula
a✝¹ : IsSub phi✝ v✝ t✝ phi'✝
a✝ : IsSub psi✝ v✝ t✝ psi'✝
a_ih✝¹ : Rec.fastReplaceFree v✝ t✝ phi✝ = phi'✝
a_ih✝ : Rec.fastReplaceFree v✝ t✝ psi✝ = psi'✝
⊢ (Rec.fastReplaceFree v✝ t✝ phi✝).imp_ (Rec.fastReplaceFree v✝ t✝ psi✝) = phi'✝.imp_ psi'✝

case and_
F F' : Formula
v u : VarName
phi✝ psi✝ : Formula
v✝ t✝ : VarName
phi'✝ psi'✝ : Formula
a✝¹ : IsSub phi✝ v✝ t✝ phi'✝
a✝ : IsSub psi✝ v✝ t✝ psi'✝
a_ih✝¹ : Rec.fastReplaceFree v✝ t✝ phi✝ = phi'✝
a_ih✝ : Rec.fastReplaceFree v✝ t✝ psi✝ = psi'✝
⊢ (Rec.fastReplaceFree v✝ t✝ phi✝).and_ (Rec.fastReplaceFree v✝ t✝ psi✝) = phi'✝.and_ psi'✝

case or_
F F' : Formula
v u : VarName
phi✝ psi✝ : Formula
v✝ t✝ : VarName
phi'✝ psi'✝ : Formula
a✝¹ : IsSub phi✝ v✝ t✝ phi'✝
a✝ : IsSub psi✝ v✝ t✝ psi'✝
a_ih✝¹ : Rec.fastReplaceFree v✝ t✝ phi✝ = phi'✝
a_ih✝ : Rec.fastReplaceFree v✝ t✝ psi✝ = psi'✝
⊢ (Rec.fastReplaceFree v✝ t✝ phi✝).or_ (Rec.fastReplaceFree v✝ t✝ psi✝) = phi'✝.or_ psi'✝

case iff_
F F' : Formula
v u : VarName
phi✝ psi✝ : Formula
v✝ t✝ : VarName
phi'✝ psi'✝ : Formula
a✝¹ : IsSub phi✝ v✝ t✝ phi'✝
a✝ : IsSub psi✝ v✝ t✝ psi'✝
a_ih✝¹ : Rec.fastReplaceFree v✝ t✝ phi✝ = phi'✝
a_ih✝ : Rec.fastReplaceFree v✝ t✝ psi✝ = psi'✝
⊢ (Rec.fastReplaceFree v✝ t✝ phi✝).iff_ (Rec.fastReplaceFree v✝ t✝ psi✝) = phi'✝.iff_ psi'✝

case forall_not_free_in
F F' : Formula
v u x✝ : VarName
phi✝ : Formula
v✝ t✝ : VarName
a✝ : ¬isFreeIn v✝ (forall_ x✝ phi✝)
⊢ (if v✝ = x✝ then forall_ x✝ phi✝ else forall_ x✝ (Rec.fastReplaceFree v✝ t✝ phi✝)) = forall_ x✝ phi✝

case forall_free_in
F F' : Formula
v u x✝ : VarName
phi✝ : Formula
v✝ t✝ : VarName
phi'✝ : Formula
a✝² : isFreeIn v✝ (forall_ x✝ phi✝)
a✝¹ : ¬x✝ = t✝
a✝ : IsSub phi✝ v✝ t✝ phi'✝
a_ih✝ : Rec.fastReplaceFree v✝ t✝ phi✝ = phi'✝
⊢ (if v✝ = x✝ then forall_ x✝ phi✝ else forall_ x✝ (Rec.fastReplaceFree v✝ t✝ phi✝)) = forall_ x✝ phi'✝

case exists_not_free_in
F F' : Formula
v u x✝ : VarName
phi✝ : Formula
v✝ t✝ : VarName
a✝ : ¬isFreeIn v✝ (exists_ x✝ phi✝)
⊢ (if v✝ = x✝ then exists_ x✝ phi✝ else exists_ x✝ (Rec.fastReplaceFree v✝ t✝ phi✝)) = exists_ x✝ phi✝

case exists_free_in
F F' : Formula
v u x✝ : VarName
phi✝ : Formula
v✝ t✝ : VarName
phi'✝ : Formula
a✝² : isFreeIn v✝ (exists_ x✝ phi✝)
a✝¹ : ¬x✝ = t✝
a✝ : IsSub phi✝ v✝ t✝ phi'✝
a_ih✝ : Rec.fastReplaceFree v✝ t✝ phi✝ = phi'✝
⊢ (if v✝ = x✝ then exists_ x✝ phi✝ else exists_ x✝ (Rec.fastReplaceFree v✝ t✝ phi✝)) = exists_ x✝ phi'✝