Replace `Sequent` type with theorems reasoning on the semantics of a sequent

[EnguerrandPrebet]

[EnguerrandPrebet]

The more I think of it, the more I am unsure whether it would be a good idea to re-implement sequent calculus.
The JAR'17 paper mentions rules but not sequent per se (both premises and conclusion are plain formulas).

I really feel that sticking which semantics proofs works the best (by using Formula.eval) and using Lean's calculus.

[eneoli]

I really feel that sticking which semantics proofs works the best (by using Formula.eval) and using Lean's calculus.

+1