proposition: Lemma long_path_occur : is_restricted R l -> forall x y m, path R x y m -> length m >= length l - 1 -> exists z, occur eqdec z (x :: m ++ y :: nil) >= 2.
proof: Proof. intros. apply pigeon_hole with l. apply restricted_path_incl. apply H. apply H0. simpl. rewrite length_app. simpl. lia. Qed.
imports: CoLoR(RelSub ListUtil ListNodup RelUtil LogicUtil ListShrink NatUtil ListOccur)