Substitution bellow quantifier (#203)

* Add the file CHANGES.md

* tracking inconsistencies

* implement a first version of substeq2

* tracking a bug

* 2-version works

* removed all version, renamed versions 2 to normal. All seems to work (including Recursion.scala). Haven't run tests yet, nor tested on function substitutions

* All tests and the library work. Added sanity checks for substitution steps.

* Add tests

* scalafix, scalafmt

* update CHANGES.md

* "of" for quantified facts has been implemented and tested.

* manual and changelist updated,  order between forall and free instantiation swapped. scalafix, scalafmt.

* correct typos