(define add1
   <> -> <> 
   (@v N V) -> (@v (+ N 1) (add1 V)))