fixpoint "--rewrite"

constant sum : (func(0, [int; int]))

define sum(n : int) : int = { if (n <= 0) then (0) else (n + sum (n-1)) }


expand [1 : True]
expand [2 : True]

bind 0 n : {v : int | (3 <= v) }

constraint:
  env []
  lhs {v : int | true }
  rhs {v : int | (sum 5) = 15 }
  id 1 tag []