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