Swithed from goal to type level functions

  Added Theorem data type
  Fixed examples