(defun subeq (x y) (if (endp x) t (if (mem (first x) y) (subeq (rest x) y) nil))) Theorem. (implies (and (not (endp a)) (not (endp (rest a))) (not (mem (first (rest a)) b))) (equal (subeq a b) nil)) Proof. My goal is to prove: (implies (and (not (endp a)) (not (endp (rest a))) (not (mem (first (rest a)) b))) (equal (subeq a b) nil)) = {def subeq} (implies (and (not (endp a)) (not (endp (rest a))) (not (mem (first (rest a)) b))) (equal (if (endp a) t (if (mem (first a) b) (subeq (rest a) b) nil)) nil)) = {hyp} (implies (and (not (endp a)) (not (endp (rest a))) (not (mem (first (rest a)) b))) (equal (if nil t (if (mem (first a) b) (subeq (rest a) b) nil)) nil)) = {(if nil x y) = y} (implies (and (not (endp a)) (not (endp (rest a))) (not (mem (first (rest a)) b))) (equal (if (mem (first a) b) (subeq (rest a) b) nil) nil)) = {def subeq} (implies (and (not (endp a)) (not (endp (rest a))) (not (mem (first (rest a)) b))) (equal (if (mem (first a) b) (if (endp (rest a)) t (if (mem (first (rest a)) b) (subeq (rest (rest a)) b) nil)) nil) nil)) = {hyp} (implies (and (not (endp a)) (not (endp (rest a))) (not (mem (first (rest a)) b))) (equal (if (mem (first a) b) (if nil t (if (mem (first (rest a)) b) (subeq (rest (rest a)) b) nil)) nil) nil)) = {(if nil x y) = y} (implies (and (not (endp a)) (not (endp (rest a))) (not (mem (first (rest a)) b))) (equal (if (mem (first a) b) (if (mem (first (rest a)) b) (subeq (rest (rest a)) b) nil) nil) nil)) = {hyp} (implies (and (not (endp a)) (not (endp (rest a))) (not (mem (first (rest a)) b))) (equal (if (mem (first a) b) (if nil (subeq (rest (rest a)) b) nil) nil) nil)) = {(if nil x y) = y} (implies (and (not (endp a)) (not (endp (rest a))) (not (mem (first (rest a)) b))) (equal (if (mem (first a) b) nil nil) nil)) = {if-x-y-y: (if x y y) = y} (implies (and (not (endp a)) (not (endp (rest a))) (not (mem (first (rest a)) b))) (equal nil nil)) = {x=x} (implies (and (not (endp a)) (not (endp (rest a))) (not (mem (first (rest a)) b))) t) = {(implies p t) = t} t Q.E.D.