PARTIAL COMMIT:

PARTIAL COMMIT:
 The whole logic of the guarded_by_constructors is being changed.
 The new idea is this one:
  1) The guarded_by_constructors is applied to a term t which must always
     generate an inhabitant of an inductive data type or of a co-inductive
     data type.
  2) When it find a constructor in head position, then the constructor
     must construct the inductive or co-inductive data type of 1).
  3) The type of the formal parameter of a constructor determines what
     condition is checked on the actual parameters of the constructors:
     a) Not recursive: the function must not occur in the actual parameter
     b) Simply recursive (to be defined): the function must occur in the
        actual parameter only guarded by constructors (where the constructor
        has already been found).
     c) Imbricated (i.e. it is another inductive type applied to the one
        that is going to be recursively defined): in this case the guarded
        by constructors (where the constructor has already been found) must
        be called, but:
         I) the expected inductive data type is no more the old one, but
            the one of the inductive data type that is in head position in
            the type.
        II) Once (if) one constructor of I) will be found, its type must
            be considered only after the substitution of the left (?)
            parameters and considering recursion IN THE CO-INDUCTIVE TYPE
            THAT IS THE OUTPUT TYPE OF THE WHOLE COFIX.

What is still wrong with this commit is that we don't have the notion of
imbricated argument yet. So, as soon as an imbricated argument is found,
the invariant 1-3 are broken and sooner or later an exception is raised
or false is returned.