Remove preconditions from axioms [not yet ready for review]

[typerSniper]

This is the PR for removing the preconditions from consequence and definition axioms. Its a work in progress with several more bugs still to fix. Please see the commit messages at from Aug 26-27 for each detail.

1. By adding can calls to the post-condition of the function, we are able to perform induction : because we assume the canCall (and thus the consequence axiom) for every input != actual input. This with the decreases check for termination makes sure that this is sound (See FibWithExtraPost in dafny0/FunctionSpecifications.dfy)

2. Cascading requires requires obligations can be avoided by canCall: performance + pruning (elaborate). Performance-wise it saves the solver from having to prove pre-conditions (in order to use consequence/definition axioms) repeatedly. Technically speaking, in order to prove a method/lemma/function, only the following functions are necessary:

     1. the functions mentioned (spec + implementation) in the method/lemma/function -- level 1
     2. the pre-conditions of level 1 functions -- level 2
     3. function-ensures-body*(level 1 + level 2)
   

   That is, everything reachable from the preconditions of level 2 can be safely pruned away. Once this PR works, this should happen automatically!

3. The isA for case BinaryExpr.ResolvedOpcode.NeqCommon: only needs to be added when exactly one of e.E1 and e.E2 is both: a DatatypeValue and Nullary.

4. This is a bit lazy but I didn't get time to check the following line in Translator.cs:
   var canCallImp = BplImp(canCallFunc, canCallOverridingFunc);
   Specifically, I am unsure of the order of arguments. This corresponds to giving can calls in the override axiom. The best way is to generate code and check it, which I should soon. But I'm semi-confident, this is correct as it is. A test for this seems important.

[RustanLeino]

Oh, no! I clicked the "marked this pull request as ready for review now" button by mistake. I will revert to the old-fashioned way of writing "[not yet ready for review]" in the title.

[MikaelMayer]

Oh, no! I clicked the "marked this pull request as ready for review now" button by mistake. I will revert to the old-fashioned way of writing "[not yet ready for review]" in the title.

I think you can still revert it to draft, see below: