proposition: Lemma path_headP : forall l x y, path x y l -> R x (nth 0 l y).
proof: Proof. induction l. intros. simpl. simpl in H. auto. intros. simpl. simpl in H. intuition. Qed.
imports: CoLoR(RelSub ListUtil ListNodup RelUtil LogicUtil ListShrink NatUtil ListOccur)