proposition: Fact map_S_list_an a n : map S (list_an a n) = list_an (S a) n.
proof: Proof. revert a; induction n; simpl; intro; f_equal; auto. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)