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