proposition: Lemma dp_elim_vars : 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 /\ incl (vars t) (vars l).
proof: Proof. intros. destruct (dp_elim H). decomp H0. exists x. intuition. trans (vars x). unfold incl. intros. eapply subterm_eq_vars. eapply in_calls_subterm. apply H3. hyp. apply hyp2. hyp. Qed.
imports: CoLoR(LogicUtil ATrs ACalls ACap ASN RelUtil ListUtil SN VecUtil VecOrd NatUtil BoolUtil)