proposition: Theorem list_injective_rect l : list_injective l -> P l.
proof: Proof. Proof using HP0 HP1. induction l as [ [ | x l ] IHl ] using (measure_rect (@length _)). intro; apply HP0. intros; apply HP1. apply list_injective_inv, H. apply IHl; simpl; auto. apply list_injective_inv with (1 := H). Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)