congr!
v t : VarName
phi : Formula
phi_ih : ¬occursIn t phi → fastReplaceFree t v (fastReplaceFree v t phi) = phi
h1 : ¬occursIn t phi
⊢ (fastReplaceFree t v (fastReplaceFree v t phi)).not_ = phi.not_
case h.e'_1
v t : VarName
phi : Formula
phi_ih : ¬occursIn t phi → fastReplaceFree t v (fastReplaceFree v t phi) = phi
h1 : ¬occursIn t phi
⊢ fastReplaceFree t v (fastReplaceFree v t phi) = phi