predicates permut over maps and arrays are given new semantics, as follows:
- MapPermut: permut m1 m2 l u means that m1[l..u[ is a permutation of
  m2[l..u[ and values outside the interval [l..u[ are *ignored*.
- ArrayPermut: permut_sub a1 a2 l u means that a1[l..u[ is a permutation
  of a2[l..u[ and other meaningful values are *identical*.
- ArrayPermut: another predicate map_permut_sub has the same semantics as
  MapPermut.permut_sub, that is values outside of the interval [l..u[
  are ignored