proposition: Lemma in_vcalls : forall x t n (ts : terms n), In x (calls t) -> Vin t ts -> In x (vcalls ts).
proof: Proof. induction ts; simpl; intros. contr. destruct H0. subst t. apply in_appl. hyp. apply in_appr. apply IHts; hyp. Qed.
imports: CoLoR(LogicUtil ATrs ListUtil VecUtil EqUtil BoolUtil) Coq(Sumbool)