I should add the context that I am concerned with strongly normalizing systems like System-F.
I have what I consider a very strong notion of equivalence for lambda terms that goes something like the following (not super formal)
- if $E_1$ and $E_2$ have WHNFs $\lambda x:t.E_1'$ and $\lambda x:t.E_2'$ then $E_1 = E_2$ if $\forall x:t. E_1' = E_2'$
- if $E_1$ and $E_2$ have WHNFs that are not $\lambda$s then they must be constructively equivalent. If $\lambda$s are elements of $E_1$ and $E_2$ they must be in the same structural locations and be equivalent by 1.
Is this notation of equivalence stronger than beta equivalence for strongly normalizing systems? If not is it equivalent? Are there stronger kinds of equivalence (or perhaps ones in the same spirit but more formal)?