simp only [fastReplaceFree_self]
case h2
P : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ P
⊢ IsDeduct Δ (fastReplaceFree v v P)
case h2
P : Formula
v : VarName
Δ : Set Formula
h1 : IsDeduct Δ P
⊢ IsDeduct Δ P