proposition: Lemma R_dec_clos_trans_restriction_dec : eq_dec A -> rel_dec R -> forall l, rel_dec (clos_trans (restriction R l)).
proof: Proof. intros. apply restricted_dec_clos_trans_dec with l. hyp. apply restriction_dec; hyp. apply restricted_restriction. Qed.
imports: Coq(Relations List Arith) CoLoR(Path RelMidex RelSub LogicUtil)