fact: Variables (P : list X -> list X -> Type) (HP0 : forall ll, P nil ll) (HP1 : forall x l ll, l <p ll -> P l ll -> P (x::l) (x::ll)).
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)