; Define
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; prefixp: TL x TL -> Bool
;
; (prefixp l1 l2) returns t if l1 is a prefix of l2

Attempt 1:

(definec prefixp (l1 :tl l2 :tl) :bool
  (cond ((endp l1) t)
        (t (and (equal (car l1) (car l2))
                (prefixp (cdr l1) (rest l2))))))


(check= (prefixp '(1 2 3) '(1 2 3)) t)
(check= (prefixp '(1) '(1 2)) t)
(check= (prefixp '(1 2 3) '(3)) nil)

Even though the tests pass, this doesn't work.
Consider:

(check= (prefixp '(2 3) '(1 2 3)) nil)
(check= (prefixp '(nil) '()) nil)

So, here is a fix:

(definec prefixp (l1 :tl l2 :tl) :bool
  (cond ((endp l1) t)
        ((endp l2) nil)
        (t (and (equal (car l1) (car l2))
                (prefixp (cdr l1) (rest l2))))))


Here is a second solution

(definec prefix2p (l1 :tl l2 :tl) :bool
  (or (endp l1)
      (and (consp l2)
           (equal (car l1) (car l2))
           (prefix2p (cdr l1) (rest l2)))))


Are prefixp and prefixp-v2 equivalent? Yes.  We'll see how to prove
that later, but let's ask ACL2s:

(thm (implies (and (tlp l1) (tlp l2))
              (equal (prefix2p l1 l2)
                     (prefixp l1 l2))))


Which one is clearer? The second.

Notice that these definitions do not follow from a "recipe".  A recipe
is good for getting started. Your code should be clean, clear,
elegant, easy to understand and modify, and, after algorithms class,
efficient.