new proofs
Added some type signatures and removed some trace statements
corrected a typo in the test case
added type signatures and removed tracing statements.