Making those proofs which depend on names generated for the arguments
in Prop of constructors of inductive types independent of these names.

Incidentally upgraded/simplified a couple of proofs, mainly in Reals.

This prepares to the next commit about using names based on H for such
hypotheses in Prop.
Use of "H"-based names for propositional hypotheses obtained by
destruction of schemes in Type such as sumbool.

Added an option "Set Standard Proposition Elimination Names" for
governing this strategy (activated by default).

This provides names supposingly more uniform than before for those who
like to have names automatically generated, at least in the first
phase of the development process of proofs.

Examples:

*** Non dependent case ***

Goal {True}+{False}-> True.
intros [|].

Before:

  t : True
  ============================
   True

and

  f : False
  ============================
   True

After:

  H : True
  ============================
   True

  H : False
  ============================
   True

*** Dependent case ***

Goal forall x:{True}+{False}, x=x.
intros [|].

Before:

  t : True
  ============================
   left t = left t

  f : False
  ============================
   right f = right f

After:

  HTrue : True
  ============================
   left HTrue = left HTrue

  HFalse : False
  ============================
   right HFalse = right HFalse
A little bit of documentation about V5.10 and V6.3 and V7.