qualif Zog(v:a, z:b) : (v = z) bind 0 x : {v : int | true} bind 1 q : {v : int | true} bind 2 y : {v : int | v = 42} constraint: env [1] lhs {v : int | v = q} rhs {v : int | $k0[x:=q] } id 1 tag [] constraint: env [2] lhs {v : int | $k0[x:=y]} rhs {v : int | v = 10} id 2 tag [] wf: env [0] reft {v : int | $k0}