// This qualifier saves the day; solve constraints WITHOUT IT qualif ListZ(v : [@(0)]): (len v >= 0) constant len : (func(2, [(@(0) @(1)); int])) bind 0 y : {v : [(Tuple int a)] | [len v >= 0]} constraint: env [0] lhs {v1 : [(Tuple int a)] | [v1 = y] } rhs {v1 : [(Tuple int a)] | [$k0[v0 := v1]] } id 1 tag [] constraint: env [] lhs {v2 : [(Tuple int a)] | [$k0[v0 := v2]] } rhs {v2 : [(Tuple int a)] | [len v2 >= 0] } id 2 tag [] wf: env [ ] reft {v0 : [(Tuple int a)] | [$k0] }