La distinción que están haciendo puede ser útil y se utiliza realmente en alguna prueba asistentes.
Hay muchas posibles reglas de reescritura en el lambda-cálculo, entre los que se destacan $\alpha$-conversión, $\beta$-reducción y $\eta$-conversión. La fundamental relación de equivalencia entre los términos es sintáctica igualdad de $\equiv$, que en general es definido de manera que contenga $\alpha$-conversión. Pero también hay otras las relaciones de equivalencia que identificar los términos que hasta la aplicación repetida de $\beta$-reducción y/o $\eta$-conversión.
Por ejemplo, intensional igualdad de $=_\beta$ entre los términos se define por las reglas:
$$\frac {M \to_\beta N} {M =_\beta N} \qquad \frac {M \equiv N} {M =_\beta N} \qquad \frac {M =_\beta N} {N =_\beta M} \qquad \frac {L =_\beta M \quad M =_\beta N} {L =_\beta N}$$
que en conjunto expresan el hecho de que $=_\beta$ es reflexiva, simétrica y transitiva cierre de $\to_\beta$.
Extensional igualdad de $=_{\beta\eta}$ es otra relación entre los términos, definidos por las normas:
$$\frac {M \to_\beta N} {M =_{\beta\eta} N} \qquad \frac {M \to_\eta N} {M =_{\beta\eta} N} \qquad \frac {M \equiv N} {M =_{\beta\eta} N} \qquad \frac {M =_{\beta\eta} N} {N =_{\beta\eta} M} \qquad \frac {L =_{\beta\eta} M \quad M =_{\beta\eta} N} {L =_{\beta\eta} N}$$
Así que, cuando decimos que dos términos son "el mismo" o "igual", es necesario especificar si estamos hablando de la igualdad sintáctica, intensional igualdad o extensional de la igualdad.
En su caso, lo que usted llama "la creación de definiciones" puede ser visto como una extensión de igualdad sintáctica de las reglas, tales como
$$\mathsf {id} \equiv \lambda x. x$$
o como darle la introducción de reglas para otra regla de reescritura que se conoce a veces como $\delta$-conversión. Uno de tales normas podrían ser
$$\mathsf {id}\, M \to_\delta M$$
que moralmente refleja el hecho de que $\mathsf {id}$ es la identidad. En este caso, podríamos definir de nuevo las relaciones de equivalencia $=_{\beta\delta}$$=_{\beta\delta\eta}$, al igual que antes, pero, respectivamente, de las reglas adicionales
$$\frac {M \to_\delta N} {M =_{\beta\delta} N} \qquad \frac {M \to_\delta N} {M =_{\beta\delta\eta} N}$$
La elección depende de lo que queremos hacer. La mayoría de las veces no tratamos $\mathsf {id}$ como un acceso directo para $\lambda x. x$, de manera que podamos elegir a considerar sintácticamente equivalentes. Pero, en algunos contextos, tiene sentido considerar también la posibilidad de $\delta$conversión: por ejemplo, en Coq el llamado "desarrollo de transparente constantes", que esencialmente corresponde a $\to_\delta$, permite volver a escribir una nueva constante sólo cuando tiene sentido hacerlo.
Observación. Hay razones por las que es preferible tener un $\mathsf{id} \, M \to_\delta M$ en lugar de $\mathsf{id} \to_\delta \lambda x. x$, ver Taroccoesbrocco los comentarios de abajo.
