proposition: Lemma clos_trans_restriction_dec_R_dec : (forall l, rel_dec (clos_trans (restriction R l))) -> rel_dec R.
proof: Proof. do 3 intro. destruct (X (x::y::nil) x y). constructor. pose incl_restriction. unfold inclusion in i. apply i with A (x::y::nil). apply clos_trans_restricted_pair. apply restricted_restriction. hyp. constructor 2. intro. pose (clos_trans_restriction R x y). tauto. Qed.
imports: Coq(Relations List Arith) CoLoR(Path RelMidex RelSub LogicUtil)