DEFTYPE and SATISFIES