Redex long tutorial beta-eta equivalence is false

[samth]

Consider the following term in the language of Lambda from https://docs.racket-lang.org/redex/redex2015.html : ((lambda () ((lambda (x) 1))) 2). This term is not beta-equivalent to anything, because it's stuck. But it is eta-equivalent to ((lambda (x) 1) 2) which beta-reduces to 1. So the statement in the tutorial

The βη semantics is equivalent to the β variant. Formulate this theorem as a metafunction. Use redex-check to test your theorem.

is wrong.

This error was found by random testing, here: http://drdr.racket-lang.org/69138/racket/share/pkgs/redex-doc/redex/scribblings/long-tut/code/lab-tue-mor.rkt