`notP` is defined twice

[affeldt-aist]

in contra.v:

analysis/classical/contra.v

Line 272 in 61acc8d

Definition notP {nP P} := MoveView (@lax_notP false nP P).

and in boolp.v:

analysis/classical/boolp.v

Line 686 in 61acc8d

Lemma notP (P : Prop) : ~ ~ P <-> P.

causing different behaviors according to which module is require imported.

[affeldt-aist]

fyi @t6s