unfold Instantiation.comp
σ σ' : 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_ (sub σ meta_var_ (sub σ' meta_var_ psi)) =
    (sub (σ.comp σ') meta_var_ phi).imp_ (sub (σ.comp σ') meta_var_ psi)
σ σ' : 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_ (sub σ meta_var_ (sub σ' meta_var_ psi)) =
    (sub ⟨↑σ ∘ ↑σ', ⋯⟩ meta_var_ phi).imp_ (sub ⟨↑σ ∘ ↑σ', ⋯⟩ meta_var_ psi)