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