proposition: Fact in_list_injective_1 x ll : ~ In x ll -> list_injective ll -> list_injective (x::ll).
proof: Proof. intros H1 H2 l a m b r H3. destruct l as [ | u l ]. inversion H3; subst. destruct m as [ | v m ]. contradict H1; subst; simpl; auto. contradict H1; subst; simpl; right; apply in_or_app; right; left; auto. inversion H3; subst. apply (H2 l _ m _ r); auto. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)