proposition: Lemma dp_elim : forall l t, In (mkRule l t) dp -> exists r, In (mkRule l r) R /\ In t (calls R r) /\ negb_subterm l t = true.
proof: Proof. intros. apply mkdp_elim. hyp. Qed.
imports: CoLoR(LogicUtil ATrs ACalls ACap ASN RelUtil ListUtil SN VecUtil VecOrd NatUtil BoolUtil)