[axioms] untracked val construct

The following construct is not tracked in hypotheses and axioms:

module Any
  predicate p (_ : int) = false
  let choose (x : int) : int
    ensures { p result }
    = val r : int ensures { p result } in r
end