case not_ phi phi_ih =>
  simp only [sub]
  simp only [Holds]
  congr! 1
  exact phi_ih V σ
D : Type
I : Interpretation D
E : Env
c : Char
phi : Formula
phi_ih : ∀ (V : VarAssignment D) (σ : VarName → VarName), Holds D I V E (sub σ c phi) ↔ Holds D I (V ∘ σ) E phi
V : VarAssignment D
σ : VarName → VarName
⊢ Holds D I V E (sub σ c phi.not_) ↔ Holds D I (V ∘ σ) E phi.not_
no goals