linter.fugue.haveBareName

have x : Y := z for a bare name z — a lone identifier, no dots — is never right. If z is a hypothesis, retyping it by defeq is change Y at z; if z is a nullary global, inline it at its use site.

A dotted right-hand side (sim.mem_agree', hpr.field) is a projection, not a bare name, and a clarifying type on it is often the point — those are left alone.