Beta equivalence

A Binary relation that relates terms connected by Beta-reduction - $(\lambda x.\ t)\ s =_\beta [x\to s]t$ - capturing the fundamental computation rule of function application.