proposition: Fact incl_left_right_cons x l y m : incl (x::l) (y::m) -> y = x /\ In y l \/ y = x /\ incl l m \/ In x m /\ incl l (y::m).
proof: Proof. intros H; apply incl_cons_linv in H. destruct H as [ [|] H2 ]; auto. apply incl_right_cons_choose in H2; tauto. Qed.
imports: Arith Lia List Permutation Relations Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)