fact: Fixpoint symb_ord_img_rec R Rc f : list Sig := match Rc with | nil => nil | a :: Rc' => if root_eq f (lhs a) && Inb (@eq_rule_dec Sig) a R then def_symbs R (rhs a) ++ symb_ord_img_rec R Rc' f else symb_ord_img_rec R Rc' f end.
imports: CoLoR(ATrs ListUtil ACalls LogicUtil RelMidex VecUtil) Coq(Relations Bool)