Assume, an extension of the lambda calculus with terms $t$ and values $v$ is defined in big-step operational semantics with evaluation relation $t \Downarrow v$.
It is intuitive to assume that $\beta$-equivalence holds, e.g.
(λx. t) unit $\equiv_\beta$ t when x is not free in t
It is however unclear to me, how $\equiv_\beta$ can be precisely defined in such a setting: Obviously, there is no small-step relation $\rightarrow_\beta$ that can be used to express a single reduction step, since the evaluation relates terms and values.
On the other hand, beta-equivalent terms do not evaluate to syntactically equal terms (e.g. when comparing abstractions which already are values).
So how does one define this equivalence in such a case?
