congr! 1
σ σ' : Instantiation
phi : Formula
phi_ih : sub σ meta_var_ (sub σ' meta_var_ phi) = sub (σ.comp σ') meta_var_ phi
⊢ (sub σ meta_var_ (sub σ' meta_var_ phi)).not_ = (sub ⟨↑σ ∘ ↑σ', ⋯⟩ meta_var_ phi).not_
no goals