Use syntax similar to functional dependencies. The injectivity declaration
begins with `|` following type family declaration head. `|` is followed by a
list of comma-separated injectivity conditions. Each injectivity condition has
the form:

{{{
result A -> B
}}}