let function : generate one axiom for each post condition

When generating spec axioms for "let function", generate one axiom of the form "forall args. precond1 -> ... -> precondn -> post_i" for each postconditon post_i, instead of using the conjunction of the postconditions.

Provers tend to not instantiate lemmas that are too big, because that have too many binders. Generating axioms of this form help them. Also, lemma generated this way are easier to use manually.

For "let lemma", we do this only if the function has no return values, because then it is not logically equivalent (because of the existential).