proposition: Lemma restricted_clos_trans : forall R l, is_restricted R l -> is_restricted (clos_trans R) l.
proof: Proof. unfold is_restricted. intros. induction H0. apply H. hyp. tauto. Qed.
imports: CoLoR(ListShrink RelUtil ListUtil LogicUtil)