minor fixes
o added event parameters
o fixed the proof obligations of the proof construct that frees universally quantified variables.
adjusted the proof obligation of transient
o Fixed inheritance of invariants
o Use inherited invariants in proof obligations
o Added inheritance of parameters
Cleaned up some warning messages