fact: Definition antisym_topo_sortable R := {F : list A -> A -> A -> bool | let G := (fun l x y => F l x y = true) in antisym R G /\ forall l, linear_extension R l (G l)}.
imports: Coq(Sumbool Arith) CoLoR(RelDec RelUtil ListUtil RelSub Path LogicUtil)