unfold IsMetaVarOrAllDefInEnv
E : Env
σ : Instantiation
τ : MetaInstantiation
x y : VarName
h1 : IsMetaVarOrAllDefInEnv E (eq_ x y)
h2 : ∀ X ∈ (eq_ x y).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ IsMetaVarOrAllDefInEnv E (eq_ (↑σ x) (↑σ y))
E : Env
σ : Instantiation
τ : MetaInstantiation
x y : VarName
h1 : IsMetaVarOrAllDefInEnv E (eq_ x y)
h2 : ∀ X ∈ (eq_ x y).metaVarSet, IsMetaVarOrAllDefInEnv E (τ X)
⊢ True