Will be supported in programs as soon, as we enable lambdas.

Since we are going to handle partial application of logical symbols,
there is no need to be rigid about currying: (((=) 0) 1) should be
(0 = 1) and not (((\ x y. x = y) @ 0) @ 1).

We do not want to generate distinct liftings for every single
partial application of a function or predicate symbol. Canonical
closures have an easily recognizable shape, thus we can detect
them and replace them with a unique constant "f_closure".

The old syntax:   abstract expr [spec]...

The semicolon binds more loosely than "abstract" and
the specification clauses are optional, so that
"abstract e1; e2" is the same as "(abstract e1); e2"
and "abstract e1; e2; ensures {...}" is a syntax error.

The new syntax:   abstract [spec]... expr end

This allows to put sequences of expressions under "abstract"
without ambiguity and moves the specification clauses to the
beginning. In other words, "abstract" becomes a "begin" with
a specification attached. The spec-at-the-top is consistent
with the syntax of functions and the whole seems to be more
natural for the intented use of "abstract" (a logical cut).

Examples:

  begin ... expr; end

  let fn x y = ... expr ; in ...

  match ... with pat -> ... expr ; | pat -> ... expr ; end

In this way, it's much easier to add and remove additional
assertions at the end of ()-typed blocks.

(used to be in Permut libraries)
new library array.ArrayPermut2, similar to ArrayPermut, but using
number of occurrences

Comment out the lemmas about symmetry of permutation:
they perturb our provers and are of little interest in
the case of successive array permutations.