proposition: Lemma LETS_irrefl : eq_midex A -> (irreflexive (clos_trans (restriction R l)) <-> irreflexive LETS).
proof: Proof. split;intros. unfold LETS. apply try_add_arc_many_to_many_irrefl; try hyp. refl. apply restricted_clos_trans. apply restricted_restriction. apply tc_trans. apply irreflexive_incl with LETS. apply LETS_restriction_clos_trans. hyp. Qed.
imports: Coq(Sumbool Arith) CoLoR(RelDec RelUtil ListUtil RelSub Path LogicUtil)