qualif Zog(v:a) : (10 <= v)
qualif Zog(v:a) : (9 <= v)
qualif Zog(v:a) : (8 <= v)
qualif Zog(v:a) : (99 <= v)

constraint:
  env []
  lhs {v : int | (v = 100)}
  rhs {v : int | $k0}
  id 1 tag []

constraint:
  env []
  lhs {v : int | $k0}
  rhs {v : int | (15 <= v) }
  id 2 tag []


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