proposition: Fact list_app_head_not_nil X (u v : list X) : u <> nil -> v <> u++v.
proof: Proof. intros H; contradict H. destruct u as [ | a u ]; auto; exfalso. apply f_equal with (f := @length _) in H. revert H; simpl; rewrite app_length; intros; lia. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)