proposition: Lemma bpath_Sn_n_or_Rn : forall n x y, bpath (S n) x y -> bpath n x y \/ exists z : A, R x z /\ bpath n z y.
proof: Proof. intros. inversion H. destruct (le_le_S_dec (length l) n). constructor. apply bp_intro with l; hyp. constructor 2. destruct l. simpl in l0. pose (Nat.nle_succ_0 n l0). tauto. exists a. simpl in H0, H1. split. tauto. apply bp_intro with l. apply le_S_n. hyp. tauto. Qed.
imports: CoLoR(RelSub ListUtil ListNodup RelUtil LogicUtil ListShrink NatUtil ListOccur)