fact: Definition symb_ord R : relation Sig := fun f g => exists a, In a R /\ root_eq f (lhs a) = true /\ In g (def_symbs R (rhs a)).
imports: CoLoR(ATrs ListUtil ACalls LogicUtil RelMidex VecUtil) Coq(Relations Bool)