proposition: Fact incl_right_cons_choose x l m : m ⊆ x::l -> x ∈ m \/ m ⊆ l.
proof: Proof. intros H; apply incl_cons_r_inv in H as ([ | y m1] & m2 & H1 & H2 & H3). + right. intros u H; apply H3; revert H. apply Permutation_in; auto. + left. apply Permutation_in with (1 := Permutation_sym H1). rewrite Forall_forall in H2. rewrite (H2 y); left; auto. Qed.
imports: Arith Lia List Permutation Undecidability.Shared.Libs.DLW.Utils(utils_tac php) Undecidability.Shared.Libs.DLW.Wf(measure_ind)