Adjust implicits of cancellation lemmas

Like injectivity lemmas, instances of cancellation lemmas (whose
conclusion is `cancel ? ?`, `{in ?, cancel ? ?}`, `pcancel`, or
`ocancel`) are passed to
generic lemmas such as `canRL` or `canLR_in`. Thus such lemmas should
not have trailing on-demand implicits _just before_ the `cancel`
conclusion, as these would be inconvenient to insert (requiring
essentially an explicit eta-expansion).
We therefore use `Arguments` or `Prenex Implicits` directives to make
all such arguments maximally inserted implicits. We don’t, however make
other arguments implicit, so as not to spoil direct instantiation of
the lemmas (in, e.g., `rewrite -[y](invmK injf)`).
We have also tried to do this with lemmas whose statement matches a
`cancel`, i.e., ending in `forall x, g (E[x]) = x` (where pattern
unification will pick up `f = fun x => E[x]`).
We also adjusted implicits of a few stray injectivity
lemmas, and defined constants.
We provide a shorthand for reindexing a bigop with a permutation.
Finally we used the new implicit signatures to simplify proofs that
use injectivity or cancellation lemmas.

1 files changed, 14 insertions, 1 deletions

diff --git a/ChangeLog b/ChangeLog
index 4f17072..b82a0f4 100644
--- a/ChangeLog
+++ b/ChangeLog
@@ -24,7 +24,20 @@
 	  from eqtype.v. They were already in ssrfun.v.
 
 	* Specialized `bool_irrelevance` so that the statement reflects
-	  the name
+	  the name.
+
+	* Changed the shape of the type of FieldMixin to allow one-line
+	  in-proof definition of bespoke fieldType structure.
+
+	* Refactored and extended Arguments directives to provide more
+	  comprehensive signature information.
+
+	* Added maximal implicits to reflection, injectivity and cancellation
+	  lemmas so that they are easier to pass to combinator lemmas such as
+	  sameP, inj_eq or canLR.
+
+	* Added reindex_inj s shorthand for reindexing a bigop with a
+	  permutation s.
 
 	* Added lemma `eqmxMunitP`: two matrices with the same shape
 	  represent the same subspace iff they differ only by a change of