Add typed beta rules for (vproj x (vin x...)) etc.

[jonsterling]

These are exactly the case that our direct computation rules cannot deal with (because it is not a stable reduction).

Also, @favonia, what happens with HITs? do we generate typed beta rules for such cases? Otherwise, it would not be possible to prove many goals that ought to be true.

An alternative is to add a single rule that lets us establish a judgmental equivalence using unstable evaluation, supposing that both sides of the equation are well-typed. This seems likely to be true (it seems like it has to be!), but I'd like someone to double check to be sure.

[favonia]

No typed beta rules for inductive types yet, and I prefer the second solution.

[cangiuli]

@favonia This shouldn't be too hard, right?

I would like to have this so I can try to finish the vproj-is-an-equivalence proof in RedPRL. As it is, there are not enough rules for V types.