proposition: Fact prefix_trans l1 l2 l3 : l1 <p l2 -> l2 <p l3 -> l1 <p l3.
proof: Proof. intros (m1 & H1) (m2 & H2); subst; exists (m1++m2); solve list eq. Qed.
imports: List Arith Lia Permutation Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac)