-pplicative_case has been rewritten and simplified;

-pplicative_case has been rewritten and simplified;
  the strategy should be clear, now.
  - if we have an unkown ?n goal we instantiate it with I:True:Prop.
    Due to the topological ordering of goals, ?n should not appear
      in any other open goal, so its instantiation can be arbitrary.
      - paramodulation is has only an implicit knowledge of the symmetry
        of equality, hence it is in trouble to prove (a=b) = (b=a).
          A try_sym tactic has been added to smart application to cover this
            case.-This line, and those below, will be ignored--

M    nnAuto.ml