Theorem: FOL.NV.Sub.Var.One.Rec.replaceFree_eq_fastReplaceFree (FOL/NV/Sub/Var/One/Rec/ReplaceFree.lean)

State before:
F : Formula
v t : VarName
⊢ replaceFree v t F = fastReplaceFree v t F
Tactic:
simp only [replaceFree]
State after:
F : Formula
v t : VarName
⊢ replaceFreeAux v t ∅ F = fastReplaceFree v t F

State before:
F : Formula
v t : VarName
⊢ replaceFreeAux v t ∅ F = fastReplaceFree v t F
Tactic:
apply replaceFreeAux_eq_fastReplaceFree
State after:
case h1
F : Formula
v t : VarName
⊢ v ∉ ∅

State before:
case h1
F : Formula
v t : VarName
⊢ v ∉ ∅
Tactic:
simp
State after:
no goals