proposition: Lemma in_vcalls_nil : forall x n (v : terms n), Vin x v -> vcalls v = nil -> calls x = nil.
proof: Proof. induction v; simpl; intros. contr. ded (app_eq_nil _ _ H0). destruct H1. destruct H. subst x. hyp. apply IHv; hyp. Qed.
imports: CoLoR(LogicUtil ATrs ListUtil VecUtil EqUtil BoolUtil) Coq(Sumbool)