Replaced induction with inversion in lemma. Fixed some naming.
Fixes to the transitive rule.
Fixes here and there.
Merge branch 'master' of https://github.com/supercooldave/ruse
Spotted bugs in the Callback and Returnback cases of the trace semantics due to the new changes introduced there.