proposition: Lemma ren_caps_sub_aux : forall s n (ts : terms n) k l, exists s', ren_caps k (Vmap (sub s) ts) = Vmap (sub s') (ren_caps l ts) /\ forall x, x < l \/ x >= l + nb_aliens_vec ts -> s' x = Var x.
proof: Proof. induction ts; intros. simpl. exists (fun x => Var x). auto. simpl. destruct (ren_cap_sub_aux s h k l) as [s1]. destruct H as [H1 H1']. rewrite H1. destruct (IHts (k + nb_aliens (sub s h)) (l + nb_aliens h)) as [s2]. destruct H as [H2 H2']. rewrite H2. set (s' := fun x => match In_dec x (vars (ren_cap l h)) with left _ => s1 x | right _ => s2 x end). exists s'. split. apply Vcons_eq_intro. apply sub_eq. intros. unfold s'. case (In_dec x (vars (ren_cap l h))); intro. refl. intuition. apply Vmap_sub_eq. intros. ded (vars_ren_caps H). unfold s'. case (In_dec x (vars (ren_cap l h))); intro. ded (vars_ren_cap i). lia. refl. rewrite nb_aliens_cons. intros. unfold s'. case (In_dec x (vars (ren_cap l h))); intro. ded (vars_ren_cap i). lia. apply H2'. lia. Qed.
imports: CoLoR(LogicUtil ACalls ATrs VecUtil ListUtil NatUtil RelUtil)