proposition: Fact map_cst_rev X Y (y : Y) ll : map (fun _ : X => y) (rev ll) = map (fun _ => y) ll.
proof: Proof. do 2 rewrite map_cst_repeat; rewrite rev_length; auto. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)