proposition: Theorem php_upto X (R : X -> X -> Prop) (l m : list X) : symmetric _ R -> transitive _ R -> (forall x, In x l -> exists y, In y m /\ R x y) -> length m < length l -> exists a x b y c, l = a++x::b++y::c /\ R x y.
proof: Proof. intros HR1 HR2 H1 H2. destruct PHP_rel with (R := R) (2 := H2) as (a & x & b & y & c & z & G1 & G2 & G3 & G4); auto. exists a, x, b, y, c; split; auto. apply (HR2 _ z); auto. Qed.
imports: Arith Lia List Permutation Relations Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)