fact: Fixpoint root_lhs_rules (R : rules) : list Sig := match R with | nil => nil | a :: R' => match lhs a with | Fun f _ => f :: root_lhs_rules R' | _ => root_lhs_rules R' end end.
imports: CoLoR(ATrs ListUtil ACalls LogicUtil RelMidex VecUtil) Coq(Relations Bool)