Make eq_pattern_test/eq_test work up to the equivalence of primitive
projections with their eta-expanded constant form.
Return a Prop not an arbitrary Type, and correct a typo.