(use  srfi-1 matchable varsubst)

(define (subst-term t subst k)
  (match t
	 (('if c t e)
	  `(if ,(k c subst) ,(k t subst) ,(k e subst)))
	 (('let bs e)
	  (k `(let ,(map (lambda (b) `(,(car b) ,(k (cadr b) subst))) bs) ,e) subst))
	 ((f . es)
	  (cons (k f subst) (map (lambda (e) (k e subst)) es)))
	 ((? atom? ) t)))

(define (binding? t) (and (list? t) (eq? 'let (car t)) (cdr t)))

(define (bind ks vs e) `(let ,(zip ks vs) ,e))

(define driver  (subst-driver (lambda (x) (and (symbol? x) x)) binding? identity bind subst-term))

(print (driver `(let ((a 1) (b 2)) (+ a (let ((a (+ b 5))) (+ a b)))) subst-empty))