proposition: Lemma in_calls_hd_red_dp : forall l r t s, In (mkRule l r) R -> In t (calls R r) -> negb_subterm l t = true -> hd_red dp (sub s l) (sub s t).
proof: Proof. intros. exists l. exists t. exists s. intuition. eapply dp_intro. apply H. hyp. hyp. Qed.
imports: CoLoR(LogicUtil ATrs ACalls ACap ASN RelUtil ListUtil SN VecUtil VecOrd NatUtil BoolUtil)