proposition: Lemma restricted_dec_clos_trans_dec : eq_dec A -> rel_dec R -> forall l, is_restricted R l -> rel_dec (clos_trans R).
proof: Proof. do 6 intro. destruct (bpath_dec (length l) H X0 x y) . constructor. apply (bpath_clos_trans b). constructor 2. intro. pose (clos_trans_bpath (eq_dec_midex X) H H0). contr. Qed.
imports: Coq(Relations List Arith) CoLoR(Path RelMidex RelSub LogicUtil)