proposition: Lemma bpath_midex : forall l n, is_restricted R l -> rel_midex R -> rel_midex (bpath R n).
proof: Proof. unfold rel_midex. induction n; intros. destruct (H0 x y). constructor. apply bp_intro with (nil : list A). trivial. simpl. hyp. constructor 2. intro. inversion H2. destruct l0. simpl in H4. contr. simpl in H3. exact (Nat.nle_succ_0 (length l0) H3). destruct (IHn H H0 x y). constructor. apply bpath_n_Sn. hyp. assert ((exists 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 midex_lem; tauto. destruct H2. destruct H2. constructor. apply R_bpath_n_Sn with x0; tauto. constructor 2. intro. destruct (bpath_Sn_n_or_Rn H3). contr. destruct H4. 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)