fixed the test oracle

added some function definitions
o New set / function theorems
o adopted a new style to classify the imports between libraries and
inter-module dependencies
o added safety properties
o added typing error messages

pos:
o made the proof steps into regular proof obligations
o merged the two "transient" proof obligations for soundness
o added renaming for event parameters in the transient proof obligation
o created proof obligation dumps
o changed the proof obligation entailment sequent to make it less
general but more efficient

syntax
o added into the syntax:
    o disjunctions
    o equivalence
    o reverse imp
    o negation and
    o universal quantifiers