The performance gain seems neglectable, unfortunatelly...

* Use sig instead of sigT: the proof is a Prop after all
* Tweak implicit arguments
* Shorten proof of sigma

It now traverses terms at most once, whereas the setoid_rewrite
approach was travering terms many times. Also, the tactic can now
be extended by defining type class instances.

Conflicts:
	barrier/barrier.v

Most notably, there is no need to internalize stuff into the logic
as it follows from generic lemmas for discrete COFEs/CMRAs.

This way it behaves better for discrete CMRAs.

Also, use "set_solver by tac" to specify a tactic.