proposition: Lemma LETS_dec : eq_dec A -> rel_dec R -> rel_dec LETS.
proof: Proof. intros. unfold LETS. apply try_add_arc_many_to_many_dec. hyp. refl. apply restricted_clos_trans. apply restricted_restriction. apply R_dec_clos_trans_restriction_dec; hyp. Qed.
imports: Coq(Sumbool Arith) CoLoR(RelDec RelUtil ListUtil RelSub Path LogicUtil)