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