proposition: Lemma local_global_acyclic : forall R : relation A, (forall l, exists R', (restriction R l) << R' /\ transitive R' /\ irreflexive R') -> irreflexive (clos_trans R).
proof: Proof. intros. do 2 intro. destruct (clos_trans_path H0). assert (clos_trans (restriction R (x::x::x0)) x x). apply path_clos_trans with x0. apply path_restriction. hyp. destruct (H (x::x::x0)). destruct H3. destruct H4. apply H5 with x. apply trans_tc_incl. hyp. apply tc_incl with (restriction R (x :: x :: x0)). hyp. hyp. Qed.
imports: Coq(Sumbool Arith) CoLoR(RelDec RelUtil ListUtil RelSub Path LogicUtil)