proposition: Lemma iter_le_bpath : forall n x y, iter_le n x y -> bpath R n x y .
proof: Proof. intros. rewrite iter_le_spec in H; destruct H as [j]; destruct H. ded (iter_path _ _ _ H0); destruct H1 as [l]; destruct H1. eapply bp_intro; try ehyp; auto; subst; hyp. Qed.
imports: Coq(List) CoLoR(Path NatUtil RelUtil LogicUtil Log2)