fixpoint "--eliminate=some" constant thinginess : func(0, [Tree; int]) constraint: env [ ] lhs {v : Tree | 666 < thinginess v } rhs {v : Tree | $k1 } id 1 tag [] constraint: env [ ] lhs {v : Tree | $k1 } rhs {v : Tree | 0 < thinginess v } id 2 tag [] wf: env [ ] reft { v: Tree | $k1 }