Vector Forall Lemmas, for all!

Lemmas for vec and Forall.

It would be good to make these lemmas consistent with the list versions, Forall_insert and Forall_replicate (and possibly derive them from those).

added 8 commits

• 067f875c...fd17255c - 7 commits from branch iris:master
• 10ace431 - vec Forall

Compare with previous version

added 1 commit

• 2b675d44 - proved new vec Forall lemmas in terms of list lemmas, and made them more similar to them

Compare with previous version

left review comments

I think this MR is fine. Please add a CHANGELOG.

added 1 commit

• b0ff6b19 - changelog

Compare with previous version

left review comments

Put short proofs on one line.

left review comments

added 1 commit

• 7ccb5a20 - Put short proofs on one line.

Compare with previous version

resolved all threads

enabled an automatic merge when all merge checks for 7ccb5a20 pass

mentioned in commit 8f987b68

merged

mentioned in merge request !606 (merged)