induction_ty_arg_lex expected behavior

This is to investigate the behavior of induction_ty_arg_lex that apparently does not do induction on the right elements.

It was reported by users that on this:

goal list_simpl_r :
  forall l1:list 'a, l2:list 'a, l:list 'a. (l1 ++ l) = (l2 ++ l) -> l1 = l2 

It was impossible to make a recursion on l1.

This issue should also investigate what changed in induction_ty_lex between 0.88 and 1.00 (on this same goal): apparently, the transformation is less clever.