proposition: Lemma ren_caps_app : forall n2 (v2 : terms n2) n1 (v1 : terms n1) k, ren_caps k (Vapp v1 v2) = Vapp (ren_caps k v1) (ren_caps (k + nb_aliens_vec v1) v2).
proof: Proof. induction v1; simpl; intros. unfold nb_aliens_vec. simpl. rewrite Nat.add_0_r. refl. rewrite nb_aliens_cons, Nat.add_assoc, <- IHv1. refl. Qed.
imports: CoLoR(LogicUtil ACalls ATrs VecUtil ListUtil NatUtil RelUtil)