TODO HORN-SMTLIB Liquid-Fixpoint Copyright 2013-21 Regents of the University of California. All Rights Reserved. (if (<= n 0) 0 (+ n (sum (- n 1))))