proposition: Lemma dp_intro : forall l r t, In (mkRule l r) R -> In t (calls R r) -> negb_subterm l t = true -> In (mkRule l t) dp.
proof: Proof. intros. ded (in_elim H). do 2 destruct H2. ded (in_elim H0). do 2 destruct H3. unfold dp. rewrite H2, mkdp_app. simpl. rewrite H3, filter_app, map_app. simpl. rewrite H1. apply in_appr. apply in_appl. apply in_appr. apply in_eq. Qed.
imports: CoLoR(LogicUtil ATrs ACalls ACap ASN RelUtil ListUtil SN VecUtil VecOrd NatUtil BoolUtil)