proposition: Lemma nb_aliens_ren_cap : forall t k, nb_aliens (ren_cap k t) = nb_aliens t.
proof: Proof. intro t; pattern t; apply term_ind with (Q := fun n (ts : terms n) => forall k, nb_aliens_vec (ren_caps k ts) = nb_aliens_vec ts); clear t; intros; auto. rewrite ren_cap_fun, nb_aliens_fun. case_eq (defined f R); intro H0. refl. rewrite nb_aliens_fun, H0. auto. simpl. rewrite !nb_aliens_cons. auto. Qed.
imports: CoLoR(LogicUtil ACalls ATrs VecUtil ListUtil NatUtil RelUtil)