case not_ phi phi_ih =>
  exact phi_ih σ
c : Char
phi : Formula
phi_ih : ∀ (σ : VarName → VarName), (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
σ : VarName → VarName
⊢ (sub σ c phi).freeVarSet = Finset.image σ phi.freeVarSet
no goals