-applicative_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.