more uniform variable naming convention

[affeldt-aist]

• enforce the convention of using T, U for names of variables
  in Type (or choiceType an pointedType)
  • as a consequence functions are of type T -> U
  • use I when the type corresponds to an index
• enforce the convention that sets are named A, B, C, D, etc.
  • indexed sets are rather named F
  • use X for set T and Y for set U when it makes sense when
    we are talking about images/preimages
  • keep X for sets of pairs
• small reordering of lemmas in sections (basic_lemmas,
  image_lemmas, bigop_lemmas) to take advantage of Implicit Types

[CohenCyril]

I'd rather reuse the convetions from mathcomp/ssreflect/finset.v

• enforce the convention of using T, U for names of variables
  in Type (or choiceType an pointedType)

Use T (if multiple types, use a suffix as in T' or T1 ... Tn or a prefix as in aT for domain type or rT return type)

• use I when the type corresponds to an index

Use I or J for indexes.

• enforce the convention that sets are named A, B, C, D, etc.

Yes

• indexed sets are rather named F
• use X for set T and Y for set U when it makes sense when

Use the same sufix or prefix for the sets as their containing type (e.g. A1 in T1, etc)

we are talking about images/preimages

• keep X for sets of pairs

or remove the suffix? (e.g. A : set (T1 * T2))

• small reordering of lemmas in sections (basic_lemmas,
  image_lemmas, bigop_lemmas) to take advantage of Implicit Types

[CohenCyril]

• document these choices in the header?

[CohenCyril]

LGTM

[CohenCyril]

Please rebase and then we merge