qualif Zog(v:a) : (10 <= v)
qualif Bog(v:a, x:a) : (x <= v)

bind 0 a : {v: int | [$k0]}

constraint:
  env [ ]
  grd true
  lhs {v : int | [v = 10]}
  rhs {v : int | [$k0]}
  id 1 

constraint:
  env [ ]
  grd true 
  lhs {v : int | [v = 20]}
  rhs {v : int | [$k0]}
  id 2 

constraint:
  env [ 0
      ]
  grd true 
  lhs {v : int | [v = a]}
  rhs {v : int | [10 <= v]}
  id 3 

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