case eq_ x y =>
  unfold IsMetaVarOrAllDefInEnv
  simp only
E : Env
σ : Instantiation
τ : MetaInstantiation
x y : VarName
h1 : IsMetaVarOrAllDefInEnv E (sub σ τ (eq_ x y))
⊢ IsMetaVarOrAllDefInEnv E (eq_ x y)
no goals