proposition: Lemma clos_trans_bpath : eq_midex A -> forall l, is_restricted R l -> R! << bpath (length l).
proof: Proof. do 6 intro. destruct (clos_trans_path H1). destruct (path_nodup_length H y x0 x H2). apply bp_intro with x1. apply nodup_midex_incl_length. hyp. tauto. apply path_restricted_incl with y x;tauto. tauto. Qed.
imports: CoLoR(RelSub ListUtil ListNodup RelUtil LogicUtil ListShrink NatUtil ListOccur)