SICP 1.14 exercise implemented as dependent type inhabited by values which represent CountChange evaluation tree