Fix: incorrect pruning of axiom with monomorhphization. (dafny-lang#4396

)

An axiom in DafnyPrelude was incorrectly being pruned away with the
`monomorphic` type encoding, because it was losing its (polymorphic)
quantifier and trigger. This meant automatic edge inference from
triggers was no longer applicable. Moved the axiom in question into a
uses clause to prevent it from being pruned.

The change has no affect on other type encodings `arguments` (current
default) and `predicates`.

There is more discussion related to the fix here in [Boogie PR
767](boogie-org/boogie#767).

<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

@@ -967,8 +967,9 @@ type Seq T;
 function Seq#Length<T>(Seq T): int;
 axiom (forall<T> s: Seq T :: { Seq#Length(s) } 0 <= Seq#Length(s));
 
-function Seq#Empty<T>(): Seq T;
-axiom (forall<T> :: { Seq#Empty(): Seq T } Seq#Length(Seq#Empty(): Seq T) == 0);
+function Seq#Empty<T>(): Seq T uses {
+  axiom (forall<T> :: { Seq#Empty(): Seq T } Seq#Length(Seq#Empty(): Seq T) == 0);
+}
 axiom (forall<T> s: Seq T :: { Seq#Length(s) }
   (Seq#Length(s) == 0 ==> s == Seq#Empty())
 // The following would be a nice fact to include, because it would enable verifying the