cases 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 ∧ IsMetaVarOrAllDefInEnv E psi
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi) ∧ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ psi)
case intro
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)
left✝ : IsMetaVarOrAllDefInEnv E phi
right✝ : IsMetaVarOrAllDefInEnv E psi
⊢ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ phi) ∧ IsMetaVarOrAllDefInEnv E (sub σ meta_var_ psi)