fact: Fixpoint list_defined (l : rules) : list Sig := match l with | nil => nil | r :: l' => match lhs r with | Var _ => list_defined l' | Fun f ts => f :: list_defined l' end end.
imports: CoLoR(LogicUtil ATrs ListUtil VecUtil EqUtil BoolUtil) Coq(Sumbool)