proposition: Lemma bpath_clos_trans : forall n, bpath n << R!.
proof: Proof. repeat intro. inversion H. apply path_clos_trans with l. hyp. Qed.
imports: CoLoR(RelSub ListUtil ListNodup RelUtil LogicUtil ListShrink NatUtil ListOccur)