fixpoint "--allowho"

data Vec 1 = [
  | VCons { head : @(0) } 
]

bind 0 foo : {v: Vec (func(0, [int; int])) | true} 

constraint:
  env [0]
  lhs {v : int | (head foo 0) = 0 }
  rhs {v : int | (head foo 0) = 0 }
  id 1 tag []