fix: use more precise types for `move_requires_*`

[TWal]

... and add move_requires_4, a companion to forall_intro_4 that was missing.

I noticed that move_requires_n don't use dependent types like forall_intro_n do, which I needed, hence this PR.

[mtzguido]

Thanks Théophile! This looks good. Just that somehow it makes LowStar.Monotonic.Buffer go into an infinite loop... I'll take a look but I killed the CI for now.

[mtzguido]

Apparently randomly, this query was causing Z3 to go into an infinite loop without burning rlimit. Some tweaks avoid. It's a good reminder to bump the default Z3 version.

Thanks again, sorry for the snafu.