Notation conflict with standard library

[jwiegley]

If you import Equations.Prop.DepElim, you cannot also import Coq.QArith.QArith. The former defines:

Notation "p # t" := (transport _ p t) (right associativity, at level 65) : equations_scope.

while the latter defines:

Notation "a # b" := (Qmake a b) (at level 55, no associativity) : Q_scope.

[mattam82]

Hmm, we should use a Module then.