fact: Fixpoint mkdp (S : rules) : rules := match S with | nil => nil | a :: S' => let (l, r) := a in map (mkRule l) (filter (negb_subterm l) (calls R r)) ++ mkdp S' end.
imports: CoLoR(LogicUtil ATrs ACalls ACap ASN RelUtil ListUtil SN VecUtil VecOrd NatUtil BoolUtil)