Add some automation to `All_Forall` for proving via `nth_error`

[JasonGross]

I got fed up trying to manually prove some weakening properties across checker configuration, and wanted a stronger hammer for dealing with things like All and Forall.

The existing strategy of combining Foralls in the context and then trying to prove the property universally is lossy when there are goals like Forall (Forall2 P l1) l2 lying around, because it doesn't guarantee that all relevant hypotheses are found. Instead, we can convert all hypotheses to nth_error and try to carefully specialize hypotheses so that nth_errors line up.

[mattam82]

Indeed, that's a more general approach and it would be great to have this!

[JasonGross]

Unfortunately, this seems to result in a bunch of universe errors down the line, and I ran out of time trying to debug them :-/