Support for quantifiers in asserts and assumes

[nchong-at-aws]

Requested feature: Allow quantifiers in Kani asserts and assumes
Use case: CBMC supports bounded quantification under constant lower and upper bounds [0]. It would be great to have this in Kani too.

[0] https://github.com/diffblue/cbmc/blob/0a69a64e4481473d62496f9975730d24f194884a/doc/cprover-manual/contracts-quantifiers.md

Link to relevant documentation (Rust reference, Nomicon, RFC): N/A
Is this a breaking change? No

Possible syntax, inspired by Prusti:

fn main() {
    let xs: [i32; 4] = kani::any();
    kani::assume(
        kani::forall(|i: usize| (0 <= i && i < 4) ==> (0 <= xs[i] && xs[i] < 1024)));
}

[tautschnig]

Was resolved with #3993.