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