proposition: Lemma mkdp_elim : forall l t S, In (mkRule l t) (mkdp S) -> exists r, In (mkRule l r) S /\ In t (calls R r) /\ negb_subterm l t = true.
proof: Proof. induction S; simpl; intros. contr. destruct a. rewrite in_app in H. destruct H. destruct (in_map_elim H). destruct H0. injection H1. intros. subst x. subst lhs. clear H1. rewrite filter_In in H0. destruct H0. exists rhs. intuition. destruct (IHS H). destruct H0. destruct H1. exists x. intuition. Qed.
imports: CoLoR(LogicUtil ATrs ACalls ACap ASN RelUtil ListUtil SN VecUtil VecOrd NatUtil BoolUtil)