Fix `smaller` predicates for reflections

[W95Psp]

Hi,

I was using the reflection API in a total context and found some inspect_* primitive were lacking refinements, forcing me to add admits about termination of some of my functions.

Hence, this PR adds refinements on the builtins inspect_bv, inspect_lb and inspect_binder to specify that inspecting a bv/lb/binder x results in a view that is smaller than x. It also fixes and simplifies some of those smaller functions that sometimes missed some << relations.