proposition: Lemma LETS_restricted : is_restricted LETS l.
proof: Proof. unfold LETS. intros. apply restricted_try_add_arc_many_to_many. refl. apply restricted_clos_trans. apply restricted_restriction. Qed.
imports: Coq(Sumbool Arith) CoLoR(RelDec RelUtil ListUtil RelSub Path LogicUtil)