// qualif Goob(v:a, z: b) : (v = z)
// qualif Prefix2(v:a, x as (mon . $1) : b, y as (sun . $1)) : (v = x + y)
qualif Prefix(v:a, z as ($1 . sday) : b) : (v = z)

bind 0  monday  : {v : int | true}
bind 10 tuesday : {v : int | true}

bind 1 q : {v : int | true}
bind 2 y : {v : int | v = 10}
bind 3 r : {v : int | true }
bind 4 s : {v : int | $k0[monday := r] } 
bind 5 t : {v : int | v = r + 1   }  

constraint:
  env [1]
  lhs {v : int | v = q}
  rhs {v : int | $k0[monday := q] }
  id 1 tag []

constraint: 
  env [3; 4; 5]
  lhs {v : int | v = s + 1 }
  rhs {v : int | $k0[monday := t] }
  id 2 tag []

constraint:
  env [2]
  lhs {v : int | $k0[monday := y]}
  rhs {v : int | v = 10}
  id 3 tag []

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