proposition: Fact incl_right_cons_incl_or_lhd_or_perm m x l : incl m (x::l) -> incl m l \/ list_has_dup m \/ exists m', m ~p x::m' /\ incl m' l.
proof: Proof. intros H. apply incl_cons_rinv in H. destruct H as (m1 & m2 & H1 & H2 & H3). destruct (repeat_choice_two H2) as [ (?&?) | [|] ]; subst m1; simpl in H1; clear H2. + right; left; apply perm_list_has_dup with (1 := Permutation_sym H1), in_list_hd0; left; auto. + left; revert H1 H3; apply perm_incl_left. + firstorder. Qed.
imports: Arith Lia List Permutation Relations Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)