simplify; (* XXX la apply non fa simplify? *)
apply congr_S; apply (IH l);
(* XXX qualcosa di enorme e' rotto! la regola di convertibilita?! *)
simplify; (* XXX la apply non fa simplify? *)
apply congr_S; apply (IH l);
(* XXX qualcosa di enorme e' rotto! la regola di convertibilita?! *)