case imp_ phi psi phi_ih psi_ih =>
  simp only [sub]
  unfold Instantiation.comp
  congr! 1
σ σ' : Instantiation
phi psi : Formula
phi_ih : sub σ meta_var_ (sub σ' meta_var_ phi) = sub (σ.comp σ') meta_var_ phi
psi_ih : sub σ meta_var_ (sub σ' meta_var_ psi) = sub (σ.comp σ') meta_var_ psi
⊢ sub σ meta_var_ (sub σ' meta_var_ (phi.imp_ psi)) = sub (σ.comp σ') meta_var_ (phi.imp_ psi)
no goals