constructor
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_left : IsMetaVarOrAllDefInEnv E (sub σ τ phi)
h1_right : IsMetaVarOrAllDefInEnv E (sub σ τ psi)
⊢ IsMetaVarOrAllDefInEnv E phi ∧ IsMetaVarOrAllDefInEnv E psi
case left
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_left : IsMetaVarOrAllDefInEnv E (sub σ τ phi)
h1_right : IsMetaVarOrAllDefInEnv E (sub σ τ psi)
⊢ IsMetaVarOrAllDefInEnv E phi

case right
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_left : IsMetaVarOrAllDefInEnv E (sub σ τ phi)
h1_right : IsMetaVarOrAllDefInEnv E (sub σ τ psi)
⊢ IsMetaVarOrAllDefInEnv E psi