op position in "type-relation" premise should refer directly to parameter

[Stephen Chang]

It would be useful if the op in a "type-relation" referred to the actual parameter. That would allow writing relations other than current-typecheck-relation. Eg, sometimes I might actually want type=