Permutations and other extensions to seq; fintype documentation

- Added `permutations` and some `perm_eq` lemmas suggested by @MrSet
  in #299 (except the link to the coq lib `Permutation` predicate).
  Use insertions to construct permutations. This definition is closer
  to the one proposed by @MrSet, than one using rotations (it adds one
  line to the definition of `permutations` but the proofs become a
  little simpler.)

- Added support for casts on `map` comprehension general terms.

- Added `allpairs_map[lr]` suggested by @pi8027 in #314, but with
  equational proofs; changed `allpairs_comp` to its converse
  `map_allpairs` for consistency.

- Add three `allpairs` extensionality lemmas: for the non-localised,
  dependent localised and non-dependent localised cases; as per
  `eq_in_map`, the latter two are equivalences.

- Documented the `all2` predicate added in #224, and the view
  combinators added in #202.

- Renamed `seq2_ind` to `seq_ind2`, and weakened the induction
  hypothesis, adding a `size` equality assumption.

- Corrected the header to use `<=>` for `bool` predicate
  documentation, and `<->` for `Prop` predicates, following the
  library’s general convention.

- Replaced the `nosimpl` in `rev` with a `Arguments simpl never`
  directive, making it possible to merge the `Rev` section into the
  main `Sequences` section.

- Miscellaneous improvements to proof scripts and file organisation.

- Correct maximal implicits of `constant`.

- Fixes omitted `Prenex Implicit` declaration.

- Other implicits fixes.

- Fix apparent `done` regression It appears `done` now does a weaker
  form of intros, and this broke the `dtuple_onP` proof. Updated the
  proof to eliminate the issue.

(Commit log edited by @CohenCyril during the squash.)

0 files changed, 0 insertions, 0 deletions