proposition: Lemma restricted_midex_clos_trans_midex : eq_midex A -> rel_midex R -> forall l, is_restricted R l -> rel_midex (clos_trans R).
proof: Proof. do 6 intro. destruct (bpath_midex (length l) H1 H0 x y) . constructor. apply (bpath_clos_trans H2). constructor 2. intro. pose (clos_trans_bpath H H1 H3). contr. Qed.
imports: Coq(Relations List Arith) CoLoR(Path RelMidex RelSub LogicUtil)