proposition: Lemma ren_caps_sub : forall s n (ts : terms n) k, exists s', ren_caps k (Vmap (sub s) ts) = Vmap (sub s') (ren_caps k ts) /\ forall x, x < k \/ x >= k + nb_aliens_vec ts -> s' x = Var x.
proof: Proof. intros. apply ren_caps_sub_aux with (l := k). Qed.
imports: CoLoR(LogicUtil ACalls ATrs VecUtil ListUtil NatUtil RelUtil)