Fix #3238

[mtzguido]

This PR fixes #3238 by changing the typing axiom for the encoded range constants.

The way we do this now is by adding the following snippet to the prelude of the encoding:

                (declare-fun Prims.isPrimitiveRangeType (Term) Term)
                (declare-fun Range_const (Int) Term)
                (assert (forall ((i Int) (ty Term))
                  (! (implies
                      (Valid (Prims.isPrimitiveRangeType ty))
                      (HasTypeZ (Range_const i) ty))
                      :pattern ((Prims.isPrimitiveRangeType ty) (Range_const i))
                      )))

Essentially this is declaring
1- The way we construct the abstract range constants, i.e. Range_const i, using a fresh i for every constant
2- A typing axiom for it. The axiom essentially says that, for any type ty such that Valid (Prims.isPrimitiveRangeType ty), all range constants are typeable at this type. The only type satisfying this will be FStar.Range.__range, but we cannot mention it here (and forward declaring a definition from such a module seems unwise). So we use this indirection, which is defined in prims, and state the following axiom in FStar.Range.fsti:

assume new type __range

assume RangePrimitive : isPrimitiveRangeType __range