Are there stronger notions of equivalence over lambda terms than beta equivalence?
Alright I'll give it a crack. It seems what you are describing is close to contextual equivalence, which is defined in the following manner $t$ and $t'$ ($t\simeq t'$) are contextually equivalent iff:

$$\forall E, E[t]\!\downarrow\ \Leftrightarrow\ E[t']\!\downarrow $$
where $E$ ranges over the set of term contexts (terms with one "hole") and $t\!\downarrow$ means $t$ is normalizing. Now this definition works for all untyped $\lambda$-terms and it is possible to show that if $t$ and $t'$ are normalizing, then
$$ t\simeq t'\ \Leftrightarrow\ t=_{\beta\eta}t'$$

Here $\beta$ is the usual $\beta$-conversion and $\eta$ is the equality
$$ \lambda x.t\ x = t$$
if $x\not\in \mathrm{FV}(t)$

This shows that $\beta+\eta$ is a rather strong form of equivalence for normalizing terms in the untyped setting. However in general the statement
$$ \forall v:T,\ t\ v=_{\beta\eta} t'\ v\qquad (1)$$
in some (normalizing) typed calculus is significatnly stronger than $t=_{\beta\eta}t'$: the first one is usually undecidable, and the second is not.



If You take as a starting point $\beta+\eta$ equality at non-functional types and $(1)$ at functional types, what you get is extensional equality of terms, and it holds in most "natural" models. See e.g. Berardi et al for models of system $F$ and the classic Barendregt chapters 5 and 10.