proposition: Lemma clos_trans_restriction : forall (R : relation A) x y, R x y -> clos_trans (restriction R (x :: y :: nil)) x y.
proof: Proof. intros. constructor. unfold restriction. simpl. tauto. Qed.
imports: CoLoR(ListShrink RelUtil ListUtil LogicUtil)