proposition: Fact incl_left_right_cons x l y m : x::l ⊆ y::m -> y = x /\ y ∈ l \/ y = x /\ l ⊆ m \/ x ∈ m /\ l ⊆ y::m.
proof: Proof. intros H; apply incl_cons_l_inv in H as [ [|] H2 ]; auto. apply incl_right_cons_choose in H2; tauto. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils_tac php) Undecidability.Shared.Libs.DLW.Wf(measure_ind)