Add some automation to All_Forall for proving via nth_error

The existing strategy of combining `Forall`s 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_error`s line up.