proposition: Lemma restriction_monotonic : forall (R' R'' : relation A) l, R' << R'' -> restriction R' l << restriction R'' l.
proof: Proof. unfold restriction. repeat intro. pose (H x y). tauto. Qed.
imports: CoLoR(ListShrink RelUtil ListUtil LogicUtil)