---

       # MATH illustrate pairs
[hear] (define cons (? x / ? y / ? f / f (x) (y)));

[hear] (define car
          (? pair /
           pair (? x / ? y / x)));

[hear] (define cdr
          (? pair /
           pair (? x / ? y / y)));

[hear] (assign x (cons 0 4) / = (car / x) 0);

[hear] (assign x (cons 0 4) / = (cdr / x) 4);

[hear] (assign x (cons 6 2) / = (car / x) 6);

[hear] (assign x (cons 6 2) / = (cdr / x) 2);

[hear] (assign x (cons 3 9) / = (car / x) 3);

[hear] (assign x (cons 3 9) / = (cdr / x) 9);

[hear] (assign x (cons 7 / cons 10 2) /
         = (car / x) 7);

[hear] (assign x (cons 7 / cons 10 2) /
         = (car / cdr / x) 10);

[hear] (assign x (cons 7 / cons 10 2) /
         = (cdr / cdr / x) 2);

[hear] (assign x (cons 1 / cons 15 17) /
         = (car / x) 1);

[hear] (assign x (cons 1 / cons 15 17) /
         = (car / cdr / x) 15);

[hear] (assign x (cons 1 / cons 15 17) /
         = (cdr / cdr / x) 17);

[hear] (assign x (cons 8 / cons 14 9) /
         = (car / x) 8);

[hear] (assign x (cons 8 / cons 14 9) /
         = (car / cdr / x) 14);

[hear] (assign x (cons 8 / cons 14 9) /
         = (cdr / cdr / x) 9);

[hear] (assign
          x
          (cons 3 /
           cons 0 /
           cons 2 /
           cons 4 1) /
         and (= 3 / car / x) /
         and (= 0 / car / cdr / x) /
         and (= 2 / car / cdr / cdr / x) /
         and (= 4 /
              car /
              cdr /
              cdr /
              cdr /
              x)
             (= 1 /
              cdr /
              cdr /
              cdr /
              cdr /
              x));