proposition: Lemma path_nth_inP : forall l x y k, path x y l -> S k < length l -> R (nth k l y) (nth (S k) l y).
proof: Proof. induction l. intros. simpl in H0. lia. intros. simpl in H. simpl in H0. gen (NatCompat.lt_n_Sm_le H0); intro. simpl. induction k. induction l. simpl. simpl in H. intuition. simpl. simpl in H. intuition. clear IHk. apply (IHl a y k). intuition. lia. Qed.
imports: CoLoR(RelSub ListUtil ListNodup RelUtil LogicUtil ListShrink NatUtil ListOccur)