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