ローカル名と修飾名

impI, assoc, transとかは、誰でもどこでも使いそうな名前なので、まずバッティングするだろう。find_theorems name: で検索して、修飾されたフルネームで指定するのが安全。