proposition: Fact list_app_inj X (l1 l2 r1 r2 : list X) : length l1 = length l2 -> l1++r1 = l2++r2 -> l1 = l2 /\ r1 = r2.
proof: Proof. revert l2; induction l1 as [ | x l1 IH ]; intros [ | y l2 ]; try discriminate. simpl; auto. intros H1 H2; inversion H1; inversion H2. apply IH in H4; auto. split; f_equal; tauto. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)