case not_ phi phi_ih =>
  congr!
  exact phi_ih h1
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_
no goals