How to use Ltac while notation "_ |- _ \in _" is defined?

[sven--]

[sven--]

Explicitly describe it? such as
(has_type _ _ _) <=> ( _ |- _ \in _).
There also might be something corresponds to context_rule
(??? _ _) <=> ( _ |- _)

[sven--]

http://coq.inria.fr/refman/Reference-Manual008.html#hevea_command133
Not worked on ( _ |- _ )

[sven--]

One possible solution : NOT defining notation that contains "|-"?