proposition: Lemma R_midex_clos_trans_restriction_midex : eq_midex A -> rel_midex R -> forall l, rel_midex (clos_trans (restriction R l)).
proof: Proof. intros. apply restricted_midex_clos_trans_midex with l. hyp. apply restriction_midex; hyp. apply restricted_restriction. Qed.
imports: Coq(Relations List Arith) CoLoR(Path RelMidex RelSub LogicUtil)