proposition: Lemma R_bpath_n_Sn : forall x y z n, R x y -> bpath n y z -> bpath (S n) x z.
proof: Proof. intros. inversion H0. apply bp_intro with (y::l). simpl. apply le_n_S. hyp. simpl. tauto. Qed.
imports: CoLoR(RelSub ListUtil ListNodup RelUtil LogicUtil ListShrink NatUtil ListOccur)