When a function is admitted to the logic, ACL2 tries to ``guess''
what type of object it returns. This guess is codified as a term
that expresses a property of the value of the function. For app
the term is
(OR (CONSP (APP X Y)) (EQUAL (APP X Y) Y))which says that
app
returns either a cons or its second argument.
This formula is added to ACL2's rule base as a type-prescription
You should now return to the Walking Tour.