qualif Prefix2(v:a, x as (sun . $1)  : b, y as (mon . $1) : b) : (v = x + y)

bind 0  sunday  : {v : int | v = 6  }
bind 1  monday  : {v : int | v = 4  }
bind 2  tuesday : {v : int | v = 10 }

bind 10 x       : {v : int | v = 4  }
bind 11 y       : {v : int | v = 6  }
bind 12 z       : {v : int | v = 10 }

constraint:
  env [10; 11; 12]
  lhs {v : int | v = 10 }
  rhs {v : int | $k0[sunday := x][monday := y][ tuesday := z] }
  id 1 tag []

constraint: 
  env [10; 11; 12]
  lhs {v : int | $k0[sunday := x][monday := y][ tuesday := z] }
  rhs {v : int | v = 10 }
  id 2 tag []

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