Fix Unfold, Axiom, and Def in the presence of shadowing

[favonia]

This is a note that the current conversion checker is incorrect in the presence of shadowing, because the constructs Domain.Unfold, Domain.Axiom, Syntax.Axiom, Syntax.Def only remember the top-level names provided by the user. The checker could potentially mistake heads with the same top-level names as judgmentally equal, depending on whether unfolding is forced. A correct implementation should instead use a more globally unique identifier, such as a pair of a file path and its index in that unit (e.g., "/cool/lib.ag", 10). I would like to address this issue only after rewriting the bantorra library (a library for unit path resolution).