proposition: Fact incl_left_right_php x l y m : incl (y::m) (x::l) -> list_has_dup (y::m) \/ x = y /\ incl m l \/ In y l /\ incl m l \/ In y l /\ exists m', m ~p x::m' /\ incl m' l.
proof: Proof. intros H; apply incl_left_right_cons in H. destruct H as [ (? & ?) | [ (? & ?) | (H1 & H2) ] ]; subst; auto. + left; apply in_list_hd0; auto. + apply incl_right_cons_incl_or_lhd_or_perm in H2; firstorder. left; apply in_list_hd1; auto. Qed.
imports: Arith Lia List Permutation Relations Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)