proposition: Lemma calls_capa : forall t m, calls (fcap (capa t) (fresh m (nb_aliens t))) = nil.
proof: Proof. set (Q := fun n (ts : terms n) => forall m, vcalls (Vmap_sum (Vmap capa ts) (fresh m (sum (Vmap capa ts)))) = nil). intro. pattern t. apply term_ind with (Q := Q); clear t; intros. refl. unfold nb_aliens. simpl. pattern (defined f R). apply bool_eq_ind; intros; simpl. refl. rewrite H0. apply H. unfold Q. refl. unfold Q. simpl. intro. rewrite fresh_plus, Vbreak_app. simpl. apply app_nil. apply H. apply H0. Qed.
imports: Coq(Sumbool) CoLoR(LogicUtil ACalls ATrs VecUtil ListUtil NatUtil EqUtil)