unfold IsMetaVarOrAllDefInEnv at h1
E : Env
σ : Instantiation
phi psi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E phi → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi)
psi_ih : IsMetaVarOrAllDefInEnv E psi → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ psi)
h1 : IsMetaVarOrAllDefInEnv E (phi.imp_ psi)
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ (phi.imp_ psi))
E : Env
σ : Instantiation
phi psi : Formula
phi_ih : IsMetaVarOrAllDefInEnv E phi → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi)
psi_ih : IsMetaVarOrAllDefInEnv E psi → IsMetaVarOrAllDefInEnv E (sub σ meta_var_ psi)
h1 : IsMetaVarOrAllDefInEnv E phi ∧ IsMetaVarOrAllDefInEnv E psi
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ (phi.imp_ psi))