proposition: Lemma restriction_dec : eq_dec A -> rel_dec R -> rel_dec restriction.
proof: Proof. unfold restriction. intros H H0 x y. destruct (H0 x y). destruct (In_dec H x l). destruct (In_dec H y l). constructor. tauto. constructor 2. tauto. constructor 2. tauto. constructor 2. tauto. Qed.
imports: CoLoR(ListShrink RelUtil ListUtil LogicUtil)