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.