Formatting ithelement definition
Adding Tactic Notation for induction on traces.
Moved trace tactic notation to a separate file and added trace_pattern_cases as well.
Merge branch 'master' of github.com:cimbriano/mtocoq
Adding case notation. Not entirely sure about i > 2 SSCase in concat Case