proposition: Theorem PHP_rel : exists a x b y c v, l = a++x::b++y::c /\ In v m /\ R x v /\ R y v.
proof: Proof. Proof using Hlm image_R_l. destruct image_R_l as (Rl & H1 & H2). destruct finite_pigeon_hole with (2 := H1) as (v & x & y & z & H). + apply Forall2_length in H2; lia. + subst Rl. apply Forall2_app_inv_r in H2; destruct H2 as (x' & l1 & H3 & H2 & ?); subst. apply Forall2_cons_inv_r in H2; destruct H2 as (v' & l2 & H4 & ? & H2); subst. apply Forall2_app_inv_r in H2; destruct H2 as (y' & l3 & H5 & H2 & ?); subst. apply Forall2_cons_inv_r in H2; destruct H2 as (v'' & l4 & H6 & ? & H2); subst. exists x', v', y', v'', l4, v; repeat (split; auto). apply H1, in_or_app; simpl; auto. Qed.
imports: Arith Lia List Permutation Relations Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)