In frame 26 we get the definition for cons0:
(degree (conso a d p)
(== `(,a ■ ,d) p))
The book hasn't mentioned yet what these black cubes are supposed to do. What does it mean?
One hint is in frame 3-4 where it is mentioned that '(d a t e ■ s)
is not a proper list.
That's just a dot:
(defrel (cons° a d p) (== `(,a . ,d) p))
The obsession with the quasiquote is quite unhelpful here, in my opinion. It seem much easier to me to read when written as the equivalent
(defrel (cons° a d p) (== (cons a d) p))