Vec.Properties: drop eq parameter when it is a property (v3.0 changes)

[mildsunrise]

Follow up to #2430 with the changes for v3. See #2421 for context.

[Taneb]

@mildsunrise now that the next release will be 3.0, do you want to revisit this?

[jamesmckinna]

So I couldn't help noticing, while trying to figure out the merge conflicts, that @shhyou 's original proofs made extensive use of the ... ≈[ ... ] ... syntax, whereas the proofs in this PR reinstate the explicit unfolding of that syntax into cast ... ... ≡ ... form.

Is that a Good Idea, or a Bad One?

Otherwise put: is it a style-guide/library-design precept that we don't use syntax explicitly in library modules?

[JacquesCarette]

I like the earlier syntax. [In part it is because it is a degenerate case of 'display map' where on thing holds over another, in this case, one equation over another.]

[shhyou]

No, I think this PR is not related to the difference between ... ≈[ ... ] ... and cast ... ... ≡ .... The current PR is to finish the postponed breaking changes in #2430, namely replace these lemmas on the left by their -eqFree variants on the right:

  ++-assoc _      ↦  ++-assoc-eqFree
  ++-identityʳ _  ↦  ++-identityʳ-eqFree
  unfold-∷ʳ _     ↦  unfold-∷ʳ-eqFree
  ++-∷ʳ _         ↦  ++-∷ʳ-eqFree
  ∷ʳ-++ _         ↦  ∷ʳ-++-eqFree
  reverse-++ _    ↦  reverse-++-eqFree
  ∷-ʳ++ _         ↦  ∷-ʳ++-eqFree
  ++-ʳ++ _        ↦  ++-ʳ++-eqFree
  ʳ++-ʳ++ _       ↦  ʳ++-ʳ++-eqFree

Previously, the ʳ++-ʳ++ lemmas use ... ≈[ ... ] ... syntax because they directly reason over cast equationally. What looks like "unfolding" at first sight is due to #2733's new proof strategy: from toList-injective and various toList-X lemmas, @jmougeot reuses list lemmas in Data.List.Properties to prove properties about vectors. Therefore cast is gone and plain equational reasoning suffices. I believe these differences do not fit @jamesmckinna's question.

I think the renaming from *-eqFree to * is still needed, but the current proof strategy is good.

[jamesmckinna]

Thanks @shhyou for the more refined analysis than my first superficial re-reading of this PR. And, to be clear, I think this is an important followup change! I had just been trying to get my head around it before trying to resolve the merge conflicts and then try to merge in to stdlib sooner rather than later...