add exact_vm_cast

This generalizes https://gitlab.mpi-sws.org/FP/LambdaRust-coq/merge_requests/10 into a reusable tactic.

Actually @ppedrot suggests we use something like

Ltac exact_vm_cast_I := match goal with |- ?P => vm_compute; match goal with |- True => exact_no_check (t <: P) end end.

I am not sure how to generalize that to other proof terms than I though.

Turns out that doesn't actually help at all in LambdaRust, so let's stick to what this MR suggests.

LGTM. Although it does not matter here, I prefer a lazymatch.

Okay. Also let's maybe wait until we figure out https://gitlab.mpi-sws.org/FP/LambdaRust-coq/merge_requests/10#note_25526.

Turns out this as a measurement error.

closed