unfold IsMetaVarOrAllDefInEnv
E : Env
σ : Instantiation
x y : VarName
h1 : IsMetaVarOrAllDefInEnv E (eq_ x y)
⊢ IsMetaVarOrAllDefInEnv E (eq_ (↑σ x) (↑σ y))
E : Env
σ : Instantiation
x y : VarName
h1 : IsMetaVarOrAllDefInEnv E (eq_ x y)
⊢ True