last comment was incomplete by mistake.

last comment was incomplete by mistake.

- Rationale
  The `Implied attribute will mark the eliminators generated by Coq
  7.3.1 added to the contrib of lambdadelta version 1.
  [the latest version of matita generates different eliminators to
   Prop (with dependences) so we cannot reuse them]
  However, these eliminators, even if provided, must not be taken into
  account when calculating the intrinsinc complexity of the contribution
  on the matita side (by the "probe" tool), because they are not taken into
  account on the Coq side, being `Generated by Coq.

  Note that the intrinsinc complexity we are interested in is the one
  accounting just for the user-defined objects in both contributions.

- probe: updated to handle the `Implied attribute

- .depend: updated