proposition: Lemma LETS_restriction_clos_trans : clos_trans (restriction R l) << LETS.
proof: Proof. intros. unfold LETS. apply sub_rel_try_add_arc_many_to_many. Qed.
imports: Coq(Sumbool Arith) CoLoR(RelDec RelUtil ListUtil RelSub Path LogicUtil)