Specifically, patterns such as `(={i}){1}` cause problems. For some reason this does not happen with `glob M`. MRE: ``` module M = {proc p(i:int) = {}}. equiv eqv: M.p ~ M.p: true ==> true. proc. conseq (: (={i}){1}). ```
Specifically, patterns such as
(={i}){1}cause problems. For some reason this does not happen withglob M.MRE: