New tactic system (#73)

New tactic system
Proofs can now be written using dedicated tactics and deduced steps. Tactics can be developped as object from which a SCProof can be recomputed.
Management of premises and target bottom sequent is unified, but tactics can optionally take other arguments.
Tactics can be used to construct proof using a dedicated syntax and DSL. Formally, The proof is built imperatively.
This means it is possible to write code in the middle of the proof (for example to print it) and it is possible to assign proof steps.
The library keep track of the proof being written from start to finish. A proof may look like:
```
THEOREM("fixedPointDoubleApplication") of "∀'x. 'P('x) ⇒ 'P('f('x)) ⊢ 'P('x) ⇒ 'P('f('f('x)))" PROOF {
        assume(forall(x, P(x) ==> P(f(x))))
        val base = have( (P(x) ==> P(f(x)), P(f(x)) ==> P(f(f(x)))) |- P(x) ==> P(f(f(x))))           by   Trivial
        have(() |- P(x) ==> P(f(f(x))))             by   SUBPROOF {
          have(P(f(x)) ==> P(f(f(x))) |- P(x) ==> P(f(f(x))) )                by   LeftForall(x)(base)
          andThen(() |- P(x) ==> P(f(f(x))))              by   LeftForall(f(x))
        }
      }
```
Sequent Calculus proof steps have been adapted so that they need only the minimum (often zero) explicit parameters, whcih are automatically infered.
Subproofs can also be used, and there is no need to do import management. Imports of Justifications and of proof steps of enclosing proofs are
automatically passed through the imports.
User should not use integers anymore to refer to premises, but instead provide a previous proof step or a justification directly.
On top of basic sequent calculus steps, the naive propositional solver and a tactic to instantiate forall quantifiers.
Existing proof have been translated to old sequent calculus (with every step lead by SC.) to make room for the new tactics identifiers.