proposition: Lemma vars_ren_caps : forall x n (ts : terms n) k, In x (vars_vec (ren_caps k ts)) -> k <= x /\ x < k + nb_aliens_vec ts.
proof: Proof. induction ts. simpl. intuition. simpl. intro. rewrite in_app, nb_aliens_cons. intro. destruct H. ded (vars_ren_cap H). lia. ded (IHts _ H). lia. Qed.
imports: CoLoR(LogicUtil ACalls ATrs VecUtil ListUtil NatUtil RelUtil)