The TI Explorer (4.2) is one of your problem cases -- it applies the flet'd function in the `satisfies' clause, instead of the defun'd one.