Added a check to make sure that the proofs of theorems refer to each other in an acyclic way.
Added some theorems to the indirect inequality test case
Added type signature to the functions of three modules
Added one proof and fixed a bug with the fresh variable generator.