proposition: Lemma antisym_topo_sortable_topo_sortable : forall R, antisym_topo_sortable R -> topo_sortable R.
proof: Proof. intros R H. exists (let (f,s):= H in f). intros. destruct H. destruct a. pose (H0 l). unfold linear_extension in *|-* . tauto. Qed.
imports: Coq(Sumbool Arith) CoLoR(RelDec RelUtil ListUtil RelSub Path LogicUtil)