constant mkEmp : func(1, [int; @(0)])

bind 0 junk : {v:bool | v = mkEmp 0 }
bind 1 punk : {v:int  | v = mkEmp 0 }

constraint:
  env [0; 1]
  lhs {v:int | v = mkEmp 10 }
  rhs {v:int | v = mkEmp 10 }
  id 0 tag []