proposition: Lemma vars_ren_cap : forall x t k, In x (vars (ren_cap k t)) -> k <= x /\ x < k + nb_aliens t.
proof: Proof. intros x t; pattern t; apply term_ind with (Q := fun n (ts : terms n) => forall k, In x (vars_vec (ren_caps k ts)) -> k <= x /\ x < k + nb_aliens_vec ts); clear t. unfold nb_aliens. simpl. intuition. intros f ts H k0. rewrite ren_cap_fun. unfold nb_aliens. simpl. case (defined f R). simpl. intuition. rewrite vars_fun. simpl. exact (H k0). simpl. intuition. intros t n ts h1 h2 k0. rewrite nb_aliens_cons. simpl. rewrite in_app. intro. destruct H. ded (h1 _ H). lia. ded (h2 _ H). lia. Qed.
imports: CoLoR(LogicUtil ACalls ATrs VecUtil ListUtil NatUtil RelUtil)