all functions should come with parametricity proofs

[andres-erbsen]

User developments often use stdlib functions with inputs whose natural equivalence relation does not coincide with Logc.eq: most importantly functions, but also Q, non-hprop sigma types, etc. Then they eventually need the fact that (forall x y, x = y -> f x = g y) -> stdlibfunc f a = stdlibfunc g a. stdlib should make lemmas of this form easily accessible, ideally in a systematic auto-generated form.

[gmalecha]

We should definitely derive things like this automatically via template-coq (see https://github.com/aa755/paramcoq-iff). Generating them would guarantee that naming is consistent and make it easy for new user-defined types to use similar conventions.

[Blaisorblade]

Such lemmas should arguably have type Proper ... stdlibfunc, and often be typeclass instances (unless they are not applicable by typeclass search).