I've often attributed this to Rules of definitional reflection by Schroeder-Heister, though the idea goes back beyond that to Girard and others; the rule you're looking for is an instance of the first display in Section 4. You also, however, need a rule that says that if the unification instance is unsatisfiable, then the assumption of equality has the force of a contradiction.
A more general account has been used recently in a lot of work by Dale Miller, David Baelde, and company (see, for instance, Least and greatest fixed points in linear logic). The more general formulation - which also doesn't originate with Miller et al - is that the rule is
$${\{\theta \in {\sf csu}(t,s) \mid \theta\Gamma \vdash \theta{C} \}}\over{\Gamma, t \doteq s \vdash C}$$
where ${\sf csu}(t,s)$ is the complete set of unifiers - the set of all unifying substitutions of $t$ and $s$. You might also prefer the equivalent way of writing this rule that I prefer (see here for example).
$${\forall \theta. \theta{t} = \theta{s} \longrightarrow \theta\Gamma \vdash \theta{C}}\over{\Gamma, t \doteq s \vdash C}$$
In any case, in a term language with decidable unification where the existence of a unifier implies the existence of a most general unifier, having either of these rules above can be shown to be equivalent to having these two rules:
$$
{{{\sf no~mgu}(t,s)}\over{\Gamma, t \doteq s \vdash C}}
\qquad
{{{\sf mgu}(t,s) = \theta \quad \theta\Gamma \vdash \theta{C}}\over{\Gamma, t \doteq s \vdash C}}
$$
(P.S. Frank discussed this in his logic programming course in lectures 6, 7, and 8, which may be where you remember it from.)
