(define c-t-aux
  (lambda (t s)
    (cond
      ((null? t) (cons '() s))
      ((symbol? t) (cons t s))
      ((pair? (car t))
       (let* ((res (c-t-aux (car t) s))
              (res2 (c-t-aux (cdr t) (cdr res))))
         (cons (cons (car res) (car res2)) (cdr res2))))
      ((var? (car t))
       (cond
         ((assq (car t) s) => (lambda (x)
                                (let ((res (c-t-aux (cdr t) s)))
                                  (cons (cons (cdr x) (car res)) (cdr res)))))
         (else (let ((v (var (gensym))))
                 (let ((res (c-t-aux (cdr t) (cons `(,(car t) . ,v) s))))
                   (cons (cons v (car res)) (cdr res)))))))
      (else (let ((res (c-t-aux (cdr t) s)))
              (cons (cons (car t) (car res)) (cdr res)))))))

(define copy-termo
  (lambda (v1 v2)
    (project (v1 v2)
      (cond
        [(var? v1) (== v1 (car (c-t-aux v2 '())))]
        [(var? v2) (== v2 (car (c-t-aux v1 '())))]
        [else (error 'copy-termo "neither side is fresh")]))))

(define instantiate-termo
  (lambda (v1 v2)
    (project (v1 v2)
      (lambdag@ (p)
        ((== v2 (reify v1 p)) p)))))