simp only [sub]
σ σ' : Instantiation
x : VarName
phi : Formula
phi_ih : sub σ meta_var_ (sub σ' meta_var_ phi) = sub (σ.comp σ') meta_var_ phi
⊢ sub σ meta_var_ (sub σ' meta_var_ (forall_ x phi)) = sub (σ.comp σ') meta_var_ (forall_ x phi)
σ σ' : Instantiation
x : VarName
phi : Formula
phi_ih : sub σ meta_var_ (sub σ' meta_var_ phi) = sub (σ.comp σ') meta_var_ phi
⊢ forall_ (↑σ (↑σ' x)) (sub σ meta_var_ (sub σ' meta_var_ phi)) =
    forall_ (↑(σ.comp σ') x) (sub (σ.comp σ') meta_var_ phi)