proposition: Lemma bpath_dec : forall l n, is_restricted R l -> rel_dec R -> rel_dec (bpath R n).
proof: Proof. unfold rel_dec. induction n; intros. destruct (X x y). constructor. apply bp_intro with (nil : list A). trivial. simpl. hyp. constructor 2. intro. inversion H0. destruct l0. simpl in H2. contr. simpl in H1. exact (Nat.nle_succ_0 (length l0) H1). destruct (IHn H X x y). constructor. apply bpath_n_Sn. hyp. assert ({z : A | In z l /\ R x z /\ bpath R n z y} +{~exists z : A, In z l /\ R x z /\ bpath R n z y}). apply dec_lem; tauto. destruct X0. constructor. destruct s. apply R_bpath_n_Sn with x0; tauto. constructor 2. intro. pose (bpath_Sn_n_or_Rn H0). destruct o. contr. destruct H1. assert (exists z : A, In z l /\ R x z /\ bpath R n z y). exists x0. split. pose (H x x0). tauto. hyp. contr. Qed.
imports: Coq(Relations List Arith) CoLoR(Path RelMidex RelSub LogicUtil)