qualif Pos(v:int)   { 0 <= v }
qualif Neg(v:int)   { v <= 0 }
qualif NeqZ(v:int)  { 0 != v }
qualif False(v:int)  { 66 = 77 }

constraint:
  env []
  lhs {v1 : int | $k0[v0 := v1] }
  rhs {v1 : int | 0 < v1 + 1   }
  id 1 tag []

constraint:
  env []
  lhs {v1 : int | v1 = 10       }
  rhs {v1 : int | $k0[v0 := v1] }
  id 2 tag []


wf:
  env []
  reft {v0 : int | $k0}

//  K0(v, b) => b <= v+1