proposition: Lemma aliens_incl_calls : forall u t, Vin u (aliens (capa t)) -> In u (calls t).
proof: Proof. intros u t. pattern t. apply term_ind_forall; clear t. simpl. auto. intros f ts H. rewrite calls_fun. simpl. case (defined f R); simpl. intuition. unfold aliens. simpl. intro. ded (in_conc H0). do 2 destruct H1. ded (Vin_map H1). do 2 destruct H3. subst x. ded (Vforall_in H H3). eapply in_vcalls. apply H4. hyp. hyp. Qed.
imports: Coq(Sumbool) CoLoR(LogicUtil ACalls ATrs VecUtil ListUtil NatUtil EqUtil)