proposition: Lemma rel_dec_topo_sortable_acyclic : forall R, rel_dec R -> topo_sortable R -> irreflexive (clos_trans R).
proof: Proof. intros R Rd H. apply local_global_acyclic. intro. destruct H. exists (fun x0 y => x l x0 y=true). destruct (l0 l). tauto. Qed.
imports: Coq(Sumbool Arith) CoLoR(RelDec RelUtil ListUtil RelSub Path LogicUtil)