proposition: Fact list_injective_map X Y (f : X -> Y) ll : (forall x y, f x = f y -> x = y) -> list_injective ll -> list_injective (map f ll).
proof: Proof. intros Hf. induction 1 as [ | x l Hl IHl ] using list_injective_rect. apply in_list_injective_0. simpl; apply in_list_injective_1; auto. contradict Hl. apply in_map_iff in Hl. destruct Hl as (y & Hl & ?). apply Hf in Hl; subst; auto. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)