Test if this is a typo in prelude (#3412)

This PR fixes #3411 
Seems like one of Boogie's axiom was wrong, but it was unnoticed because
another application axiom was ignoring the wrong argument.
I added the test case of the issue.

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

Source/DafnyCore/DafnyPrelude.bpl

@@ -1018,7 +1018,7 @@ axiom (forall ty: Ty, heap: Heap, len: int, init: HandleType ::
 axiom (forall ty: Ty, heap: Heap, len: int, init: HandleType, i: int ::
   { Seq#Index(Seq#Create(ty, heap, len, init), i) }
   $IsGoodHeap(heap) && 0 <= i && i < len ==>
-  Seq#Index(Seq#Create(ty, heap, len, init), i) == Apply1(TInt, TSeq(ty), heap, init, $Box(i)));
+  Seq#Index(Seq#Create(ty, heap, len, init), i) == Apply1(TInt, ty, heap, init, $Box(i)));
 
 function Seq#Append<T>(Seq T, Seq T): Seq T;
 axiom (forall<T> s0: Seq T, s1: Seq T :: { Seq#Length(Seq#Append(s0,s1)) }

Test/git-issues/git-issue-3411.dfy

@@ -0,0 +1,7 @@
+// RUN: %baredafny verify %args "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+method Test(f: int -> int) {
+  assert seq(1, x => f(x))[0] == f(0);  // No problem
+  assert seq(1, f)[0] == f(0);  // No problem anymore
+}

Test/git-issues/git-issue-3411.dfy.expect

@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 1 verified, 0 errors

docs/dev/news/3411.fix

@@ -0,0 +1 @@
+Fixed an axiom related to sequence comprehension extraction