Add the axiom stating that Seq#Take(s, Seq#Length(s)) == s) for all…

[MikaelMayer]

… sequence s (#4194)

A trivial axiom stating Seq#Take(s, Seq#Length(s)) == s) for all sequence s. This will help deducing automatically and without using any workaround that "multiset(arr[..]) == multiset(arr[..arr.Length])" for any array arr.

Fixes #4184

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT
license.

[btwael]

I think the file Test/git-issues/git-issue-4184.dfy should be modified to the following to avoid the non-initialization of arr:

method main(arr: array<int>) {
  assert(multiset(arr[..]) == multiset(arr[..arr.Length]));
}

I don't know how to modify that in your PR.

[btwael]

It looks that the [some-proofs-only-work-without-autoTriggers.dfy](https://github.com/dafny-lang/dafny/blob/5679b3dbbba3f9f4ed3acc139e659d26a9c19aff/Test/triggers/some-proofs-only-work-without-autoTriggers.dfy] is what cause the failure of test, adding the axiom in line 23 to the prelude make the whole test file verified (with the added axiom in this PR):

axiom (forall<T> s: Seq T, i: int ::
  { Seq#Index(s, i) }
  0 <= i && i < Seq#Length(s) ==>
  Seq#Contains(s, Seq#Index(s, i)));

If we add this axiom, maybe we should just modify "some-proofs-only-work-without-autoTriggers.dfy.expect"!?
I wonder why those axioms are not already part of the default prelude file?