Use `<:` (VMcast) for instances of `exact I` in lang/tactics.v

Title says it all. This way we get the benefits of vm_compute both during the proof and at Qed time. It brings the total compilation time down to ~7:40 from ~9:20 on the CI.

/cc @robbertkrebbers