proposition: Lemma bpath_n_Sn : forall n x y, bpath n x y -> bpath (S n) x y.
proof: Proof. intros. inversion H. apply bp_intro with l. apply Nat.le_trans with n. hyp. apply Nat.le_succ_diag_r. hyp. Qed.
imports: CoLoR(RelSub ListUtil ListNodup RelUtil LogicUtil ListShrink NatUtil ListOccur)